Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_20 (Sun Microsystems Inc.) Main-Class: Alternate/Alternate

package Alternate;

public class Alternate {

    public static Tree alternate(final Tree t, final Tree s) {
        // from (Dershowitz & Jouannaud 90, p. 253)

        if (t == null) {
            return Tree.copy(s);
        } else {
            return new Tree(Tree.copy(t.left), alternate(s, t.right));
        }

    }

    public static void main(final String[] args) {
      Random.args = args;
      final Tree t = Tree.createTree();
      final Tree s = Tree.createTree();

      alternate(t, s);
    }
}


package Alternate;
public class Random {
    static String[] args;
    static int index = 0;

    public static int random() {
        if (args.length <= index) {
            return 0;
        }
        final String string = args[index];
        index++;
        if (string == null) {
            return 0;
        }
        return string.length();
    }
}


package Alternate;


public class Tree {
    Tree left;
    Tree right;
    int value;

    public Tree(final Tree l, final Tree r) {
        this.left = l;
        this.right = r;
    }

    public Tree() {
    }

    public static Tree createNode() {
        final Tree result = new Tree();
        result.value = Random.random();
        return result;
    }

    public static Tree createTree() {
        int counter = Random.random();
        if (counter == 0) {
            return null;
        }
        final Tree result = createNode();
        Tree t = result;

        while (counter > 0) {
            final int branch = Random.random();
            if (branch > 0) {
                if (t.left == null) {
                    t.left = createNode();
                    t = result;
                } else {
                    t = t.left;
                }
            } else {
                if (t.right == null) {
                    t.right = createNode();
                    t = result;
                } else {
                    t = t.right;
                }
            }
            counter--;
        }

        return result;
    }

    public static void main(final String[] args) {
        Random.args = args;
        createTree();
    }

    public static Tree copy(final Tree s) {
        if (s == null) {
            return null;
        }
        final Tree result = new Tree();
        result.left = copy(s.left);
        result.right = copy(s.right);
        return result;
    }
}

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Alternate.Alternate.main([Ljava/lang/String;)V: Graph of 190 nodes with 0 SCCs.

Alternate.Tree.createTree()LAlternate/Tree;: Graph of 396 nodes with 1 SCC.

Alternate.Alternate.alternate(LAlternate/Tree;LAlternate/Tree;)LAlternate/Tree;: Graph of 112 nodes with 0 SCCs.

Alternate.Tree.copy(LAlternate/Tree;)LAlternate/Tree;: Graph of 72 nodes with 0 SCCs.

Alternate.Tree.createNode()LAlternate/Tree;: Graph of 99 nodes with 0 SCCs.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Logs:

---

Log for SCC 0:

Generated 46 rules for P and 35 rules for R.

Combined rules. Obtained 6 rules for P and 11 rules for R.

Filtered ground terms:

Alternate.Tree(x1, x2, x3) → Alternate.Tree(x2, x3)
2799_0_copy_NONNULL(x1, x2, x3) → 2799_0_copy_NONNULL(x2, x3)
3131_1_copy_InvokeMethod(x1, x2, x3, x4, x5) → 3131_1_copy_InvokeMethod(x1, x2, x5)
3543_0_copy_Return(x1, x2) → 3543_0_copy_Return
7594_0_copy_Return(x1, x2) → 7594_0_copy_Return(x2)
7046_0_copy_Return(x1, x2) → 7046_0_copy_Return(x2)
6379_0_copy_Return(x1, x2) → 6379_0_copy_Return(x2)
3377_1_copy_InvokeMethod(x1, x2, x3, x4) → 3377_1_copy_InvokeMethod(x1, x4)
2875_0_copy_Return(x1, x2, x3) → 2875_0_copy_Return

Filtered duplicate args:

6648_1_copy_InvokeMethod(x1, x2, x3, x4) → 6648_1_copy_InvokeMethod(x1, x3, x4)
2799_0_copy_NONNULL(x1, x2) → 2799_0_copy_NONNULL(x2)

Finished conversion. Obtained 6 rules for P and 11 rules for R. System has no predefined symbols.

---

Log for SCC 1:

Generated 35 rules for P and 169 rules for R.

Combined rules. Obtained 5 rules for P and 28 rules for R.

Filtered ground terms:

6561_1_alternate_InvokeMethod(x1, x2, x3, x4, x5, x6) → 6561_1_alternate_InvokeMethod(x1, x4, x5, x6)
Alternate.Tree(x1, x2, x3) → Alternate.Tree(x2, x3)
2870_0_copy_Load(x1, x2) → 2870_0_copy_Load(x2)
2870_1_alternate_InvokeMethod(x1, x2, x3, x4, x5, x6) → 2870_1_alternate_InvokeMethod(x1, x2, x3, x6)
3543_0_copy_Return(x1, x2) → 3543_0_copy_Return
7594_0_copy_Return(x1, x2) → 7594_0_copy_Return(x2)
7046_0_copy_Return(x1, x2) → 7046_0_copy_Return(x2)
6379_0_copy_Return(x1, x2) → 6379_0_copy_Return(x2)
3030_1_alternate_InvokeMethod(x1, x2, x3, x4, x5, x6) → 3030_1_alternate_InvokeMethod(x1, x5, x6)
2875_0_copy_Return(x1, x2, x3) → 2875_0_copy_Return
3377_1_copy_InvokeMethod(x1, x2, x3, x4) → 3377_1_copy_InvokeMethod(x1, x4)
2799_0_copy_NONNULL(x1, x2, x3) → 2799_0_copy_NONNULL(x2, x3)
3131_1_copy_InvokeMethod(x1, x2, x3, x4, x5) → 3131_1_copy_InvokeMethod(x1, x2, x5)
10759_0_alternate_Return(x1, x2) → 10759_0_alternate_Return(x2)
10743_0_alternate_Return(x1, x2) → 10743_0_alternate_Return(x2)
8181_0_alternate_Return(x1, x2) → 8181_0_alternate_Return(x2)
7575_0_alternate_Return(x1, x2) → 7575_0_alternate_Return(x2)
6204_0_alternate_Return(x1, x2, x3, x4) → 6204_0_alternate_Return(x3, x4)

Filtered duplicate args:

2799_0_copy_NONNULL(x1, x2) → 2799_0_copy_NONNULL(x2)
6648_1_copy_InvokeMethod(x1, x2, x3, x4) → 6648_1_copy_InvokeMethod(x1, x3, x4)

Finished conversion. Obtained 5 rules for P and 28 rules for R. System has no predefined symbols.

---

Log for SCC 2:

Generated 204 rules for P and 195 rules for R.

Combined rules. Obtained 37 rules for P and 34 rules for R.

Filtered ground terms:

15537_0_createTree_FieldAccess(x1, x2, x3, x4, x5) → 15537_0_createTree_FieldAccess(x2, x3, x4, x5)
Alternate.Tree(x1, x2, x3) → Alternate.Tree(x2, x3)
15225_0_random_GT(x1, x2, x3) → 15225_0_random_GT(x2, x3)
15615_0_random_IntArithmetic(x1, x2, x3, x4) → 15615_0_random_IntArithmetic(x2, x3)
15116_0_createTree_LE(x1, x2, x3, x4, x5) → 15116_0_createTree_LE(x2, x3, x4, x5)
Cond_18532_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_18532_1_createTree_InvokeMethod1(x1, x3, x4, x5)
2552_0_createNode_Return(x1, x2) → 2552_0_createNode_Return
Cond_18532_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_18532_1_createTree_InvokeMethod(x1, x3, x4, x5)
2177_0_createNode_Return(x1, x2) → 2177_0_createNode_Return
18532_0_createNode_New(x1) → 18532_0_createNode_New
Cond_18633_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_18633_1_createTree_InvokeMethod1(x1, x3, x4, x5)
Cond_18633_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_18633_1_createTree_InvokeMethod(x1, x3, x4, x5)
18633_0_createNode_New(x1) → 18633_0_createNode_New
Cond_18508_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_18508_1_createTree_InvokeMethod1(x1, x3)
18508_1_createTree_InvokeMethod(x1, x2, x3, x4) → 18508_1_createTree_InvokeMethod(x1, x2)
Cond_18508_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_18508_1_createTree_InvokeMethod(x1, x3)
18508_0_createNode_New(x1) → 18508_0_createNode_New
Cond_15615_1_createTree_InvokeMethod3(x1, x2, x3, x4, x5) → Cond_15615_1_createTree_InvokeMethod3(x1, x2, x3)
Cond_18703_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_18703_1_createTree_InvokeMethod1(x1, x3, x4, x5)
Cond_18703_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_18703_1_createTree_InvokeMethod(x1, x3, x4, x5)
18703_0_createNode_New(x1) → 18703_0_createNode_New
Cond_16209_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_16209_1_createTree_InvokeMethod1(x1, x3, x4, x5)
Cond_16209_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_16209_1_createTree_InvokeMethod(x1, x3, x4, x5)
16209_0_createNode_New(x1) → 16209_0_createNode_New
Cond_15537_0_createTree_FieldAccess2(x1, x2, x3, x4, x5, x6) → Cond_15537_0_createTree_FieldAccess2(x1, x3, x4, x5, x6)
Cond_16429_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_16429_1_createTree_InvokeMethod1(x1, x3, x4, x5)
Cond_16429_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_16429_1_createTree_InvokeMethod(x1, x3, x4, x5)
16429_0_createNode_New(x1) → 16429_0_createNode_New
Cond_15537_0_createTree_FieldAccess1(x1, x2, x3, x4, x5, x6) → Cond_15537_0_createTree_FieldAccess1(x1, x3, x4, x5, x6)
Cond_16177_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_16177_1_createTree_InvokeMethod1(x1, x3)
16177_1_createTree_InvokeMethod(x1, x2, x3, x4) → 16177_1_createTree_InvokeMethod(x1, x2)
Cond_16177_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_16177_1_createTree_InvokeMethod(x1, x3)
16177_0_createNode_New(x1) → 16177_0_createNode_New
Cond_16625_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_16625_1_createTree_InvokeMethod1(x1, x3, x4, x5)
Cond_16625_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_16625_1_createTree_InvokeMethod(x1, x3, x4, x5)
16625_0_createNode_New(x1) → 16625_0_createNode_New
Cond_15537_0_createTree_FieldAccess(x1, x2, x3, x4, x5, x6) → Cond_15537_0_createTree_FieldAccess(x1, x3, x4, x5, x6)
15396_0_random_ArrayAccess(x1, x2, x3) → 15396_0_random_ArrayAccess(x2, x3)
15219_0_random_GT(x1, x2, x3) → 15219_0_random_GT(x2, x3)
Cond_15116_0_createTree_LE1(x1, x2, x3, x4, x5, x6) → Cond_15116_0_createTree_LE1(x1, x3, x4, x5, x6)
Cond_15116_0_createTree_LE(x1, x2, x3, x4, x5, x6) → Cond_15116_0_createTree_LE(x1, x3, x4, x5, x6)
2691_0_createNode_InvokeMethod(x1, x2, x3, x4) → 2691_0_createNode_InvokeMethod
java.lang.ArrayIndexOutOfBoundsException(x1) → java.lang.ArrayIndexOutOfBoundsException
java.lang.IndexOutOfBoundsException(x1) → java.lang.IndexOutOfBoundsException
java.lang.RuntimeException(x1) → java.lang.RuntimeException
java.lang.Exception(x1) → java.lang.Exception
java.lang.Throwable(x1) → java.lang.Throwable
Cond_2133_1_createNode_InvokeMethod(x1, x2, x3, x4) → Cond_2133_1_createNode_InvokeMethod(x1, x2)
2133_0_random_ArrayAccess(x1, x2, x3) → 2133_0_random_ArrayAccess(x2, x3)
2133_1_createNode_InvokeMethod(x1, x2, x3) → 2133_1_createNode_InvokeMethod(x1)
Cond_2243_1_createNode_InvokeMethod1(x1, x2, x3, x4) → Cond_2243_1_createNode_InvokeMethod1(x1, x2)
2243_0_random_IntArithmetic(x1, x2, x3, x4) → 2243_0_random_IntArithmetic(x2, x3)
2243_1_createNode_InvokeMethod(x1, x2, x3) → 2243_1_createNode_InvokeMethod(x1)
Cond_2243_1_createNode_InvokeMethod(x1, x2, x3, x4) → Cond_2243_1_createNode_InvokeMethod(x1, x2)
Cond_2175_1_createNode_InvokeMethod(x1, x2, x3, x4) → Cond_2175_1_createNode_InvokeMethod(x1, x2)
2175_0_random_ArrayAccess(x1, x2, x3) → 2175_0_random_ArrayAccess(x2, x3)
2175_1_createNode_InvokeMethod(x1, x2, x3) → 2175_1_createNode_InvokeMethod(x1)
2722_0_createNode_InvokeMethod(x1, x2, x3, x4) → 2722_0_createNode_InvokeMethod
Cond_2176_1_createNode_InvokeMethod(x1, x2, x3, x4) → Cond_2176_1_createNode_InvokeMethod(x1, x2)
2176_0_random_ArrayAccess(x1, x2, x3) → 2176_0_random_ArrayAccess(x2, x3)
2176_1_createNode_InvokeMethod(x1, x2, x3) → 2176_1_createNode_InvokeMethod(x1)
Cond_2002_1_createNode_InvokeMethod3(x1, x2, x3, x4) → Cond_2002_1_createNode_InvokeMethod3(x1, x2)
2002_0_random_GT(x1, x2, x3) → 2002_0_random_GT(x2, x3)
2002_1_createNode_InvokeMethod(x1, x2, x3) → 2002_1_createNode_InvokeMethod(x1)
Cond_2002_1_createNode_InvokeMethod2(x1, x2, x3, x4) → Cond_2002_1_createNode_InvokeMethod2(x1, x2)
Cond_2002_1_createNode_InvokeMethod1(x1, x2, x3, x4) → Cond_2002_1_createNode_InvokeMethod1(x1, x2)
Cond_2002_1_createNode_InvokeMethod(x1, x2, x3, x4) → Cond_2002_1_createNode_InvokeMethod(x1, x2)
18669_0_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 18669_0_createTree_InvokeMethod(x3, x4, x5)
18807_0_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 18807_0_createTree_InvokeMethod(x3, x4, x5)
18628_0_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 18628_0_createTree_InvokeMethod(x3)
18960_0_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 18960_0_createTree_InvokeMethod(x3, x4, x5)
16489_0_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 16489_0_createTree_InvokeMethod(x3, x4, x5)
16769_0_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 16769_0_createTree_InvokeMethod(x3, x4, x5)
16424_0_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 16424_0_createTree_InvokeMethod(x3)
16965_0_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 16965_0_createTree_InvokeMethod(x3, x4, x5)
15141_0_createTree_Return(x1, x2) → 15141_0_createTree_Return(x2)
18547_0_createNode_InvokeMethod(x1, x2, x3, x4) → 18547_0_createNode_InvokeMethod
18648_0_createNode_InvokeMethod(x1, x2, x3, x4) → 18648_0_createNode_InvokeMethod
18521_0_createNode_InvokeMethod(x1, x2, x3, x4) → 18521_0_createNode_InvokeMethod
18746_0_createNode_InvokeMethod(x1, x2, x3, x4) → 18746_0_createNode_InvokeMethod

Filtered duplicate args:

15537_0_createTree_FieldAccess(x1, x2, x3, x4) → 15537_0_createTree_FieldAccess(x1, x2, x4)
15116_0_createTree_LE(x1, x2, x3, x4) → 15116_0_createTree_LE(x2, x3, x4)
Cond_15537_0_createTree_FieldAccess2(x1, x2, x3, x4, x5) → Cond_15537_0_createTree_FieldAccess2(x1, x2, x3, x5)
Cond_15537_0_createTree_FieldAccess1(x1, x2, x3, x4, x5) → Cond_15537_0_createTree_FieldAccess1(x1, x2, x3, x5)
Cond_15537_0_createTree_FieldAccess(x1, x2, x3, x4, x5) → Cond_15537_0_createTree_FieldAccess(x1, x2, x3, x5)
Cond_15116_0_createTree_LE1(x1, x2, x3, x4, x5) → Cond_15116_0_createTree_LE1(x1, x3, x4, x5)
Cond_15116_0_createTree_LE(x1, x2, x3, x4, x5) → Cond_15116_0_createTree_LE(x1, x3, x4, x5)

Filtered all non-integer terms:

15116_0_createTree_LE(x1, x2, x3) → 15116_0_createTree_LE(x3)
Cond_15116_0_createTree_LE(x1, x2, x3, x4) → Cond_15116_0_createTree_LE(x1, x4)
15219_1_createTree_InvokeMethod(x1, x2, x3, x4) → 15219_1_createTree_InvokeMethod(x1, x2)
Cond_15116_0_createTree_LE1(x1, x2, x3, x4) → Cond_15116_0_createTree_LE1(x1, x4)
15225_1_createTree_InvokeMethod(x1, x2, x3, x4) → 15225_1_createTree_InvokeMethod(x1, x2)
Cond_15219_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_15219_1_createTree_InvokeMethod(x1, x2, x3)
15396_1_createTree_InvokeMethod(x1, x2, x3, x4) → 15396_1_createTree_InvokeMethod(x1, x2)
Cond_15396_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_15396_1_createTree_InvokeMethod(x1, x2, x3)
15615_1_createTree_InvokeMethod(x1, x2, x3, x4) → 15615_1_createTree_InvokeMethod(x1, x2)
15615_0_random_IntArithmetic(x1, x2) → 15615_0_random_IntArithmetic(x2)
Cond_15615_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_15615_1_createTree_InvokeMethod(x1, x2, x3)
15537_0_createTree_FieldAccess(x1, x2, x3) → 15537_0_createTree_FieldAccess(x1)
Alternate.Tree(x1, x2) → Alternate.Tree
Cond_15537_0_createTree_FieldAccess(x1, x2, x3, x4) → Cond_15537_0_createTree_FieldAccess(x1, x2)
16625_1_createTree_InvokeMethod(x1, x2, x3, x4) → 16625_1_createTree_InvokeMethod(x1, x2)
Cond_16625_1_createTree_InvokeMethod(x1, x2, x3, x4) → Cond_16625_1_createTree_InvokeMethod(x1, x2)
Cond_16625_1_createTree_InvokeMethod1(x1, x2, x3, x4) → Cond_16625_1_createTree_InvokeMethod1(x1, x2)
Cond_15537_0_createTree_FieldAccess1(x1, x2, x3, x4) → Cond_15537_0_createTree_FieldAccess1(x1, x2)
16429_1_createTree_InvokeMethod(x1, x2, x3, x4) → 16429_1_createTree_InvokeMethod(x1, x2)
Cond_16429_1_createTree_InvokeMethod(x1, x2, x3, x4) → Cond_16429_1_createTree_InvokeMethod(x1, x2)
Cond_16429_1_createTree_InvokeMethod1(x1, x2, x3, x4) → Cond_16429_1_createTree_InvokeMethod1(x1, x2)
Cond_15537_0_createTree_FieldAccess2(x1, x2, x3, x4) → Cond_15537_0_createTree_FieldAccess2(x1, x2)
16209_1_createTree_InvokeMethod(x1, x2, x3, x4) → 16209_1_createTree_InvokeMethod(x1, x2)
Cond_16209_1_createTree_InvokeMethod(x1, x2, x3, x4) → Cond_16209_1_createTree_InvokeMethod(x1, x2)
Cond_16209_1_createTree_InvokeMethod1(x1, x2, x3, x4) → Cond_16209_1_createTree_InvokeMethod1(x1, x2)
Cond_15615_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_15615_1_createTree_InvokeMethod1(x1, x2, x3)
Cond_15615_1_createTree_InvokeMethod2(x1, x2, x3, x4, x5) → Cond_15615_1_createTree_InvokeMethod2(x1, x2, x3)
18703_1_createTree_InvokeMethod(x1, x2, x3, x4) → 18703_1_createTree_InvokeMethod(x1, x2)
Cond_18703_1_createTree_InvokeMethod(x1, x2, x3, x4) → Cond_18703_1_createTree_InvokeMethod(x1, x2)
Cond_18703_1_createTree_InvokeMethod1(x1, x2, x3, x4) → Cond_18703_1_createTree_InvokeMethod1(x1, x2)
Cond_15615_1_createTree_InvokeMethod4(x1, x2, x3, x4, x5) → Cond_15615_1_createTree_InvokeMethod4(x1, x2, x3)
Cond_15615_1_createTree_InvokeMethod5(x1, x2, x3, x4, x5) → Cond_15615_1_createTree_InvokeMethod5(x1, x2, x3)
18633_1_createTree_InvokeMethod(x1, x2, x3, x4) → 18633_1_createTree_InvokeMethod(x1, x2)
Cond_18633_1_createTree_InvokeMethod(x1, x2, x3, x4) → Cond_18633_1_createTree_InvokeMethod(x1, x2)
Cond_18633_1_createTree_InvokeMethod1(x1, x2, x3, x4) → Cond_18633_1_createTree_InvokeMethod1(x1, x2)
Cond_15615_1_createTree_InvokeMethod6(x1, x2, x3, x4, x5) → Cond_15615_1_createTree_InvokeMethod6(x1, x2, x3)
Cond_15615_1_createTree_InvokeMethod7(x1, x2, x3, x4, x5) → Cond_15615_1_createTree_InvokeMethod7(x1, x2, x3)
18532_1_createTree_InvokeMethod(x1, x2, x3, x4) → 18532_1_createTree_InvokeMethod(x1, x2)
Cond_18532_1_createTree_InvokeMethod(x1, x2, x3, x4) → Cond_18532_1_createTree_InvokeMethod(x1, x2)
Cond_18532_1_createTree_InvokeMethod1(x1, x2, x3, x4) → Cond_18532_1_createTree_InvokeMethod1(x1, x2)
Cond_15615_1_createTree_InvokeMethod8(x1, x2, x3, x4, x5) → Cond_15615_1_createTree_InvokeMethod8(x1, x2, x3)
Cond_15225_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_15225_1_createTree_InvokeMethod(x1, x2, x3)
15141_0_createTree_Return(x1) → 15141_0_createTree_Return
16965_0_createTree_InvokeMethod(x1, x2, x3) → 16965_0_createTree_InvokeMethod(x1)
16769_0_createTree_InvokeMethod(x1, x2, x3) → 16769_0_createTree_InvokeMethod(x1)
16489_0_createTree_InvokeMethod(x1, x2, x3) → 16489_0_createTree_InvokeMethod(x1)
18960_0_createTree_InvokeMethod(x1, x2, x3) → 18960_0_createTree_InvokeMethod(x1)
18807_0_createTree_InvokeMethod(x1, x2, x3) → 18807_0_createTree_InvokeMethod(x1)
18669_0_createTree_InvokeMethod(x1, x2, x3) → 18669_0_createTree_InvokeMethod(x1)
2243_0_random_IntArithmetic(x1, x2) → 2243_0_random_IntArithmetic(x2)

Filtered all free variables:

15219_1_createTree_InvokeMethod(x1, x2) → 15219_1_createTree_InvokeMethod(x2)
15225_1_createTree_InvokeMethod(x1, x2) → 15225_1_createTree_InvokeMethod(x2)
Cond_15219_1_createTree_InvokeMethod(x1, x2, x3) → Cond_15219_1_createTree_InvokeMethod(x1, x3)
15396_1_createTree_InvokeMethod(x1, x2) → 15396_1_createTree_InvokeMethod(x2)
Cond_15396_1_createTree_InvokeMethod(x1, x2, x3) → Cond_15396_1_createTree_InvokeMethod(x1, x3)
15615_1_createTree_InvokeMethod(x1, x2) → 15615_1_createTree_InvokeMethod(x2)
Cond_15615_1_createTree_InvokeMethod(x1, x2, x3) → Cond_15615_1_createTree_InvokeMethod(x1, x3)
Cond_15615_1_createTree_InvokeMethod1(x1, x2, x3) → Cond_15615_1_createTree_InvokeMethod1(x1, x3)
Cond_15615_1_createTree_InvokeMethod2(x1, x2, x3) → Cond_15615_1_createTree_InvokeMethod2(x1, x3)
Cond_15615_1_createTree_InvokeMethod3(x1, x2, x3) → Cond_15615_1_createTree_InvokeMethod3(x1, x3)
Cond_15615_1_createTree_InvokeMethod4(x1, x2, x3) → Cond_15615_1_createTree_InvokeMethod4(x1, x3)
Cond_15615_1_createTree_InvokeMethod5(x1, x2, x3) → Cond_15615_1_createTree_InvokeMethod5(x1, x3)
Cond_15615_1_createTree_InvokeMethod6(x1, x2, x3) → Cond_15615_1_createTree_InvokeMethod6(x1, x3)
Cond_15615_1_createTree_InvokeMethod7(x1, x2, x3) → Cond_15615_1_createTree_InvokeMethod7(x1, x3)
Cond_15615_1_createTree_InvokeMethod8(x1, x2, x3) → Cond_15615_1_createTree_InvokeMethod8(x1, x3)
Cond_15225_1_createTree_InvokeMethod(x1, x2, x3) → Cond_15225_1_createTree_InvokeMethod(x1, x3)
2002_0_random_GT(x1, x2) → 2002_0_random_GT
2133_0_random_ArrayAccess(x1, x2) → 2133_0_random_ArrayAccess(x1)
ARRAY(x1, x2) → ARRAY(x1)
2175_0_random_ArrayAccess(x1, x2) → 2175_0_random_ArrayAccess(x1)
2176_0_random_ArrayAccess(x1, x2) → 2176_0_random_ArrayAccess(x1)
2243_0_random_IntArithmetic(x1) → 2243_0_random_IntArithmetic

Filtered ground terms:

Cond_2243_1_createNode_InvokeMethod1(x1, x2) → Cond_2243_1_createNode_InvokeMethod1(x1)
2243_1_createNode_InvokeMethod(x1) → 2243_1_createNode_InvokeMethod
Cond_2243_1_createNode_InvokeMethod(x1, x2) → Cond_2243_1_createNode_InvokeMethod(x1)
Cond_2002_1_createNode_InvokeMethod3(x1, x2) → Cond_2002_1_createNode_InvokeMethod3(x1)
2002_1_createNode_InvokeMethod(x1) → 2002_1_createNode_InvokeMethod
Cond_2002_1_createNode_InvokeMethod2(x1, x2) → Cond_2002_1_createNode_InvokeMethod2(x1)
Cond_2002_1_createNode_InvokeMethod1(x1, x2) → Cond_2002_1_createNode_InvokeMethod1(x1)
Cond_2002_1_createNode_InvokeMethod(x1, x2) → Cond_2002_1_createNode_InvokeMethod(x1)

Combined rules. Obtained 25 rules for P and 29 rules for R.

Finished conversion. Obtained 25 rules for P and 29 rules for R. System has predefined symbols.

(4) Complex Obligation (AND)

(5) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:
none


The ITRS R consists of the following rules:
2799_0_copy_NONNULL(NULL) → 2875_0_copy_Return
3377_1_copy_InvokeMethod(2875_0_copy_Return, NULL) → 3543_0_copy_Return
3377_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, NULL))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(NULL, NULL)))))
3377_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3))))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))))))
3377_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))))
3377_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7))))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))))))
6648_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), NULL) → 7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))
6648_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), java.lang.Object(Alternate.Tree(NULL, NULL))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(NULL, NULL)))))
6648_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5))))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))))))
6648_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))))
6648_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9))))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))))))

The integer pair graph contains the following rules and edges:
(0): 2799_0_COPY_NONNULL(java.lang.Object(Alternate.Tree(x0[0], x1[0]))) → 3131_1_COPY_INVOKEMETHOD(2799_0_copy_NONNULL(x0[0]), java.lang.Object(Alternate.Tree(x0[0], x1[0])), x0[0])
(1): 2799_0_COPY_NONNULL(java.lang.Object(Alternate.Tree(x0[1], x1[1]))) → 2799_0_COPY_NONNULL(x0[1])
(2): 3131_1_COPY_INVOKEMETHOD(2875_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, x0[2])), NULL) → 2799_0_COPY_NONNULL(x0[2])
(3): 3131_1_COPY_INVOKEMETHOD(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0[3], x1[3]))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[3], x3[3])))), x4[3])), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[3], x3[3]))))) → 2799_0_COPY_NONNULL(x4[3])
(4): 3131_1_COPY_INVOKEMETHOD(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[4], x1[4])), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[4], x3[4])), NULL)), x4[4])), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[4], x3[4])), NULL))) → 2799_0_COPY_NONNULL(x4[4])
(5): 3131_1_COPY_INVOKEMETHOD(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[5], x1[5])), java.lang.Object(Alternate.Tree(x2[5], x3[5]))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[5], x5[5])), java.lang.Object(Alternate.Tree(x6[5], x7[5])))), x8[5])), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[5], x5[5])), java.lang.Object(Alternate.Tree(x6[5], x7[5]))))) → 2799_0_COPY_NONNULL(x8[5])
(6): 3131_1_COPY_INVOKEMETHOD(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0[6])), java.lang.Object(Alternate.Tree(NULL, NULL))) → 2799_0_COPY_NONNULL(x0[6])

(0) -> (2), if ((2799_0_copy_NONNULL(x0[0]) →^* 2875_0_copy_Return)∧(java.lang.Object(Alternate.Tree(x0[0], x1[0])) →^* java.lang.Object(Alternate.Tree(NULL, x0[2])))∧(x0[0] →^* NULL))

(0) -> (3), if ((2799_0_copy_NONNULL(x0[0]) →^* 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0[3], x1[3]))))))∧(java.lang.Object(Alternate.Tree(x0[0], x1[0])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[3], x3[3])))), x4[3])))∧(x0[0] →^* java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[3], x3[3]))))))

(0) -> (4), if ((2799_0_copy_NONNULL(x0[0]) →^* 7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[4], x1[4])), NULL))))∧(java.lang.Object(Alternate.Tree(x0[0], x1[0])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[4], x3[4])), NULL)), x4[4])))∧(x0[0] →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[4], x3[4])), NULL))))

(0) -> (5), if ((2799_0_copy_NONNULL(x0[0]) →^* 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[5], x1[5])), java.lang.Object(Alternate.Tree(x2[5], x3[5]))))))∧(java.lang.Object(Alternate.Tree(x0[0], x1[0])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[5], x5[5])), java.lang.Object(Alternate.Tree(x6[5], x7[5])))), x8[5])))∧(x0[0] →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[5], x5[5])), java.lang.Object(Alternate.Tree(x6[5], x7[5]))))))

(0) -> (6), if ((2799_0_copy_NONNULL(x0[0]) →^* 3543_0_copy_Return)∧(java.lang.Object(Alternate.Tree(x0[0], x1[0])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0[6])))∧(x0[0] →^* java.lang.Object(Alternate.Tree(NULL, NULL))))

(1) -> (0), if ((x0[1] →^* java.lang.Object(Alternate.Tree(x0[0], x1[0]))))

(1) -> (1), if ((x0[1] →^* java.lang.Object(Alternate.Tree(x0[1]', x1[1]'))))

(2) -> (0), if ((x0[2] →^* java.lang.Object(Alternate.Tree(x0[0], x1[0]))))

(2) -> (1), if ((x0[2] →^* java.lang.Object(Alternate.Tree(x0[1], x1[1]))))

(3) -> (0), if ((x4[3] →^* java.lang.Object(Alternate.Tree(x0[0], x1[0]))))

(3) -> (1), if ((x4[3] →^* java.lang.Object(Alternate.Tree(x0[1], x1[1]))))

(4) -> (0), if ((x4[4] →^* java.lang.Object(Alternate.Tree(x0[0], x1[0]))))

(4) -> (1), if ((x4[4] →^* java.lang.Object(Alternate.Tree(x0[1], x1[1]))))

(5) -> (0), if ((x8[5] →^* java.lang.Object(Alternate.Tree(x0[0], x1[0]))))

(5) -> (1), if ((x8[5] →^* java.lang.Object(Alternate.Tree(x0[1], x1[1]))))

(6) -> (0), if ((x0[6] →^* java.lang.Object(Alternate.Tree(x0[0], x1[0]))))

(6) -> (1), if ((x0[6] →^* java.lang.Object(Alternate.Tree(x0[1], x1[1]))))

The set Q consists of the following terms:
2799_0_copy_NONNULL(NULL)
3377_1_copy_InvokeMethod(2875_0_copy_Return, NULL)
3377_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, NULL)))
3377_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))))
3377_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)))
3377_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))))
6648_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), NULL)
6648_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), java.lang.Object(Alternate.Tree(NULL, NULL)))
6648_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5)))))
6648_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)))
6648_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9)))))

(6) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

2799_0_COPY_NONNULL(java.lang.Object(Alternate.Tree(x0[0], x1[0]))) → 3131_1_COPY_INVOKEMETHOD(2799_0_copy_NONNULL(x0[0]), java.lang.Object(Alternate.Tree(x0[0], x1[0])), x0[0])
2799_0_COPY_NONNULL(java.lang.Object(Alternate.Tree(x0[1], x1[1]))) → 2799_0_COPY_NONNULL(x0[1])
3131_1_COPY_INVOKEMETHOD(2875_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, x0[2])), NULL) → 2799_0_COPY_NONNULL(x0[2])
3131_1_COPY_INVOKEMETHOD(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0[3], x1[3]))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[3], x3[3])))), x4[3])), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[3], x3[3]))))) → 2799_0_COPY_NONNULL(x4[3])
3131_1_COPY_INVOKEMETHOD(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[4], x1[4])), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[4], x3[4])), NULL)), x4[4])), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[4], x3[4])), NULL))) → 2799_0_COPY_NONNULL(x4[4])
3131_1_COPY_INVOKEMETHOD(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[5], x1[5])), java.lang.Object(Alternate.Tree(x2[5], x3[5]))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[5], x5[5])), java.lang.Object(Alternate.Tree(x6[5], x7[5])))), x8[5])), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[5], x5[5])), java.lang.Object(Alternate.Tree(x6[5], x7[5]))))) → 2799_0_COPY_NONNULL(x8[5])
3131_1_COPY_INVOKEMETHOD(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0[6])), java.lang.Object(Alternate.Tree(NULL, NULL))) → 2799_0_COPY_NONNULL(x0[6])

The TRS R consists of the following rules:

2799_0_copy_NONNULL(NULL) → 2875_0_copy_Return
3377_1_copy_InvokeMethod(2875_0_copy_Return, NULL) → 3543_0_copy_Return
3377_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, NULL))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(NULL, NULL)))))
3377_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3))))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))))))
3377_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))))
3377_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7))))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))))))
6648_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), NULL) → 7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))
6648_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), java.lang.Object(Alternate.Tree(NULL, NULL))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(NULL, NULL)))))
6648_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5))))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))))))
6648_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))))
6648_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9))))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))))))

The set Q consists of the following terms:

2799_0_copy_NONNULL(NULL)
3377_1_copy_InvokeMethod(2875_0_copy_Return, NULL)
3377_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, NULL)))
3377_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))))
3377_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)))
3377_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))))
6648_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), NULL)
6648_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), java.lang.Object(Alternate.Tree(NULL, NULL)))
6648_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5)))))
6648_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)))
6648_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9)))))

We have to consider all minimal (P,Q,R)-chains.

(8) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 4 less nodes.

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

3131_1_COPY_INVOKEMETHOD(2875_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, x0[2])), NULL) → 2799_0_COPY_NONNULL(x0[2])
2799_0_COPY_NONNULL(java.lang.Object(Alternate.Tree(x0[0], x1[0]))) → 3131_1_COPY_INVOKEMETHOD(2799_0_copy_NONNULL(x0[0]), java.lang.Object(Alternate.Tree(x0[0], x1[0])), x0[0])
2799_0_COPY_NONNULL(java.lang.Object(Alternate.Tree(x0[1], x1[1]))) → 2799_0_COPY_NONNULL(x0[1])

The TRS R consists of the following rules:

2799_0_copy_NONNULL(NULL) → 2875_0_copy_Return
3377_1_copy_InvokeMethod(2875_0_copy_Return, NULL) → 3543_0_copy_Return
3377_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, NULL))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(NULL, NULL)))))
3377_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3))))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))))))
3377_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))))
3377_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7))))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))))))
6648_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), NULL) → 7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))
6648_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), java.lang.Object(Alternate.Tree(NULL, NULL))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(NULL, NULL)))))
6648_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5))))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))))))
6648_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))))
6648_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9))))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))))))

The set Q consists of the following terms:

2799_0_copy_NONNULL(NULL)
3377_1_copy_InvokeMethod(2875_0_copy_Return, NULL)
3377_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, NULL)))
3377_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))))
3377_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)))
3377_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))))
6648_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), NULL)
6648_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), java.lang.Object(Alternate.Tree(NULL, NULL)))
6648_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5)))))
6648_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)))
6648_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9)))))

We have to consider all minimal (P,Q,R)-chains.

(10) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

3131_1_COPY_INVOKEMETHOD(2875_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, x0[2])), NULL) → 2799_0_COPY_NONNULL(x0[2])
2799_0_COPY_NONNULL(java.lang.Object(Alternate.Tree(x0[0], x1[0]))) → 3131_1_COPY_INVOKEMETHOD(2799_0_copy_NONNULL(x0[0]), java.lang.Object(Alternate.Tree(x0[0], x1[0])), x0[0])
2799_0_COPY_NONNULL(java.lang.Object(Alternate.Tree(x0[1], x1[1]))) → 2799_0_COPY_NONNULL(x0[1])

The TRS R consists of the following rules:

2799_0_copy_NONNULL(NULL) → 2875_0_copy_Return

The set Q consists of the following terms:

2799_0_copy_NONNULL(NULL)
3377_1_copy_InvokeMethod(2875_0_copy_Return, NULL)
3377_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, NULL)))
3377_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))))
3377_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)))
3377_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))))
6648_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), NULL)
6648_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), java.lang.Object(Alternate.Tree(NULL, NULL)))
6648_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5)))))
6648_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)))
6648_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9)))))

We have to consider all minimal (P,Q,R)-chains.

(12) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

3377_1_copy_InvokeMethod(2875_0_copy_Return, NULL)
3377_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, NULL)))
3377_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))))
3377_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)))
3377_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))))
6648_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), NULL)
6648_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), java.lang.Object(Alternate.Tree(NULL, NULL)))
6648_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5)))))
6648_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)))
6648_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9)))))

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

3131_1_COPY_INVOKEMETHOD(2875_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, x0[2])), NULL) → 2799_0_COPY_NONNULL(x0[2])
2799_0_COPY_NONNULL(java.lang.Object(Alternate.Tree(x0[0], x1[0]))) → 3131_1_COPY_INVOKEMETHOD(2799_0_copy_NONNULL(x0[0]), java.lang.Object(Alternate.Tree(x0[0], x1[0])), x0[0])
2799_0_COPY_NONNULL(java.lang.Object(Alternate.Tree(x0[1], x1[1]))) → 2799_0_COPY_NONNULL(x0[1])

The TRS R consists of the following rules:

2799_0_copy_NONNULL(NULL) → 2875_0_copy_Return

The set Q consists of the following terms:

2799_0_copy_NONNULL(NULL)

We have to consider all minimal (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• 2799_0_COPY_NONNULL(java.lang.Object(Alternate.Tree(x0[0], x1[0]))) → 3131_1_COPY_INVOKEMETHOD(2799_0_copy_NONNULL(x0[0]), java.lang.Object(Alternate.Tree(x0[0], x1[0])), x0[0])
  The graph contains the following edges 1 >= 2, 1 > 3

• 2799_0_COPY_NONNULL(java.lang.Object(Alternate.Tree(x0[1], x1[1]))) → 2799_0_COPY_NONNULL(x0[1])
  The graph contains the following edges 1 > 1

• 3131_1_COPY_INVOKEMETHOD(2875_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, x0[2])), NULL) → 2799_0_COPY_NONNULL(x0[2])
  The graph contains the following edges 2 > 1

(15) YES

(16) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:
none


The ITRS R consists of the following rules:
2870_0_copy_Load(x0) → 2799_0_copy_NONNULL(x0)
3030_1_alternate_InvokeMethod(6204_0_alternate_Return(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))), NULL, java.lang.Object(Alternate.Tree(x0, x1))) → 7575_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))))
3030_1_alternate_InvokeMethod(7575_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))), NULL) → 10743_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))))))
3030_1_alternate_InvokeMethod(8181_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))), NULL) → 10743_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))))))
3030_1_alternate_InvokeMethod(10743_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, java.lang.Object(Alternate.Tree(x1, x2))))))), java.lang.Object(Alternate.Tree(NULL, x3)), java.lang.Object(Alternate.Tree(x4, x5))) → 10743_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, java.lang.Object(Alternate.Tree(x1, x2)))))))))
3030_1_alternate_InvokeMethod(10759_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, java.lang.Object(Alternate.Tree(x3, x4))))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x5, x6)), x7)), java.lang.Object(Alternate.Tree(x8, x9))) → 10743_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, java.lang.Object(Alternate.Tree(x3, x4)))))))))
6561_1_alternate_InvokeMethod(6204_0_alternate_Return(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))), java.lang.Object(Alternate.Tree(x4, x5)), NULL, java.lang.Object(Alternate.Tree(x0, x1))) → 8181_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x2, x3)))))
6561_1_alternate_InvokeMethod(7575_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5)))), NULL) → 10759_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))))))
6561_1_alternate_InvokeMethod(8181_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9)))), NULL) → 10759_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))))))
6561_1_alternate_InvokeMethod(10743_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, java.lang.Object(Alternate.Tree(x1, x2))))))), java.lang.Object(Alternate.Tree(x3, x4)), java.lang.Object(Alternate.Tree(NULL, x5)), java.lang.Object(Alternate.Tree(x6, x7))) → 10759_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x3, x4)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, java.lang.Object(Alternate.Tree(x1, x2)))))))))
6561_1_alternate_InvokeMethod(10759_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, java.lang.Object(Alternate.Tree(x3, x4))))))), java.lang.Object(Alternate.Tree(x5, x6)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x7, x8)), x9)), java.lang.Object(Alternate.Tree(x10, x11))) → 10759_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x5, x6)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, java.lang.Object(Alternate.Tree(x3, x4)))))))))
2799_0_copy_NONNULL(NULL) → 2875_0_copy_Return
2799_0_copy_NONNULL(java.lang.Object(Alternate.Tree(x0, x1))) → 3131_1_copy_InvokeMethod(2799_0_copy_NONNULL(x0), java.lang.Object(Alternate.Tree(x0, x1)), x0)
3131_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))), x4)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3))))) → 6648_1_copy_InvokeMethod(2799_0_copy_NONNULL(x4), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))), NULL)), x4)
3131_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), x4)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL))) → 6648_1_copy_InvokeMethod(2799_0_copy_NONNULL(x4), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), NULL)), x4)
3131_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))), x8)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7))))) → 6648_1_copy_InvokeMethod(2799_0_copy_NONNULL(x8), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))), NULL)), x8)
3131_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0)), java.lang.Object(Alternate.Tree(NULL, NULL))) → 6648_1_copy_InvokeMethod(2799_0_copy_NONNULL(x0), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), NULL)), x0)
6648_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))))
6648_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9))))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))))))
6648_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), java.lang.Object(Alternate.Tree(NULL, NULL))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(NULL, NULL)))))
6648_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5))))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))))))
6648_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), NULL) → 7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))
3131_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, x0)), NULL) → 3377_1_copy_InvokeMethod(2799_0_copy_NONNULL(x0), x0)
3377_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3))))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))))))
3377_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))))
3377_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7))))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))))))
3377_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, NULL))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(NULL, NULL)))))
3377_1_copy_InvokeMethod(2875_0_copy_Return, NULL) → 3543_0_copy_Return

The integer pair graph contains the following rules and edges:
(0): 2870_1_ALTERNATE_INVOKEMETHOD(2875_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, x0[0])), java.lang.Object(Alternate.Tree(x1[0], x2[0])), NULL) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x1[0]), java.lang.Object(Alternate.Tree(x1[0], x2[0])), x0[0], x1[0])
(1): 2870_1_ALTERNATE_INVOKEMETHOD(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0[1], x1[1]))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[1], x3[1])))), x4[1])), java.lang.Object(Alternate.Tree(x5[1], x6[1])), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[1], x3[1]))))) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x5[1]), java.lang.Object(Alternate.Tree(x5[1], x6[1])), x4[1], x5[1])
(2): 2870_1_ALTERNATE_INVOKEMETHOD(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[2], x1[2])), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[2], x3[2])), NULL)), x4[2])), java.lang.Object(Alternate.Tree(x5[2], x6[2])), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[2], x3[2])), NULL))) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x5[2]), java.lang.Object(Alternate.Tree(x5[2], x6[2])), x4[2], x5[2])
(3): 2870_1_ALTERNATE_INVOKEMETHOD(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[3], x1[3])), java.lang.Object(Alternate.Tree(x2[3], x3[3]))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[3], x5[3])), java.lang.Object(Alternate.Tree(x6[3], x7[3])))), x8[3])), java.lang.Object(Alternate.Tree(x9[3], x10[3])), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[3], x5[3])), java.lang.Object(Alternate.Tree(x6[3], x7[3]))))) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x9[3]), java.lang.Object(Alternate.Tree(x9[3], x10[3])), x8[3], x9[3])
(4): 2870_1_ALTERNATE_INVOKEMETHOD(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0[4])), java.lang.Object(Alternate.Tree(x1[4], x2[4])), java.lang.Object(Alternate.Tree(NULL, NULL))) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x1[4]), java.lang.Object(Alternate.Tree(x1[4], x2[4])), x0[4], x1[4])

(0) -> (0), if ((2870_0_copy_Load(x1[0]) →^* 2875_0_copy_Return)∧(java.lang.Object(Alternate.Tree(x1[0], x2[0])) →^* java.lang.Object(Alternate.Tree(NULL, x0[0]')))∧(x0[0] →^* java.lang.Object(Alternate.Tree(x1[0]', x2[0]')))∧(x1[0] →^* NULL))

(0) -> (1), if ((2870_0_copy_Load(x1[0]) →^* 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0[1], x1[1]))))))∧(java.lang.Object(Alternate.Tree(x1[0], x2[0])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[1], x3[1])))), x4[1])))∧(x0[0] →^* java.lang.Object(Alternate.Tree(x5[1], x6[1])))∧(x1[0] →^* java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[1], x3[1]))))))

(0) -> (2), if ((2870_0_copy_Load(x1[0]) →^* 7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[2], x1[2])), NULL))))∧(java.lang.Object(Alternate.Tree(x1[0], x2[0])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[2], x3[2])), NULL)), x4[2])))∧(x0[0] →^* java.lang.Object(Alternate.Tree(x5[2], x6[2])))∧(x1[0] →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[2], x3[2])), NULL))))

(0) -> (3), if ((2870_0_copy_Load(x1[0]) →^* 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[3], x1[3])), java.lang.Object(Alternate.Tree(x2[3], x3[3]))))))∧(java.lang.Object(Alternate.Tree(x1[0], x2[0])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[3], x5[3])), java.lang.Object(Alternate.Tree(x6[3], x7[3])))), x8[3])))∧(x0[0] →^* java.lang.Object(Alternate.Tree(x9[3], x10[3])))∧(x1[0] →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[3], x5[3])), java.lang.Object(Alternate.Tree(x6[3], x7[3]))))))

(0) -> (4), if ((2870_0_copy_Load(x1[0]) →^* 3543_0_copy_Return)∧(java.lang.Object(Alternate.Tree(x1[0], x2[0])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0[4])))∧(x0[0] →^* java.lang.Object(Alternate.Tree(x1[4], x2[4])))∧(x1[0] →^* java.lang.Object(Alternate.Tree(NULL, NULL))))

(1) -> (0), if ((2870_0_copy_Load(x5[1]) →^* 2875_0_copy_Return)∧(java.lang.Object(Alternate.Tree(x5[1], x6[1])) →^* java.lang.Object(Alternate.Tree(NULL, x0[0])))∧(x4[1] →^* java.lang.Object(Alternate.Tree(x1[0], x2[0])))∧(x5[1] →^* NULL))

(1) -> (1), if ((2870_0_copy_Load(x5[1]) →^* 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0[1]', x1[1]'))))))∧(java.lang.Object(Alternate.Tree(x5[1], x6[1])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[1]', x3[1]')))), x4[1]')))∧(x4[1] →^* java.lang.Object(Alternate.Tree(x5[1]', x6[1]')))∧(x5[1] →^* java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[1]', x3[1]'))))))

(1) -> (2), if ((2870_0_copy_Load(x5[1]) →^* 7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[2], x1[2])), NULL))))∧(java.lang.Object(Alternate.Tree(x5[1], x6[1])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[2], x3[2])), NULL)), x4[2])))∧(x4[1] →^* java.lang.Object(Alternate.Tree(x5[2], x6[2])))∧(x5[1] →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[2], x3[2])), NULL))))

(1) -> (3), if ((2870_0_copy_Load(x5[1]) →^* 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[3], x1[3])), java.lang.Object(Alternate.Tree(x2[3], x3[3]))))))∧(java.lang.Object(Alternate.Tree(x5[1], x6[1])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[3], x5[3])), java.lang.Object(Alternate.Tree(x6[3], x7[3])))), x8[3])))∧(x4[1] →^* java.lang.Object(Alternate.Tree(x9[3], x10[3])))∧(x5[1] →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[3], x5[3])), java.lang.Object(Alternate.Tree(x6[3], x7[3]))))))

(1) -> (4), if ((2870_0_copy_Load(x5[1]) →^* 3543_0_copy_Return)∧(java.lang.Object(Alternate.Tree(x5[1], x6[1])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0[4])))∧(x4[1] →^* java.lang.Object(Alternate.Tree(x1[4], x2[4])))∧(x5[1] →^* java.lang.Object(Alternate.Tree(NULL, NULL))))

(2) -> (0), if ((2870_0_copy_Load(x5[2]) →^* 2875_0_copy_Return)∧(java.lang.Object(Alternate.Tree(x5[2], x6[2])) →^* java.lang.Object(Alternate.Tree(NULL, x0[0])))∧(x4[2] →^* java.lang.Object(Alternate.Tree(x1[0], x2[0])))∧(x5[2] →^* NULL))

(2) -> (1), if ((2870_0_copy_Load(x5[2]) →^* 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0[1], x1[1]))))))∧(java.lang.Object(Alternate.Tree(x5[2], x6[2])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[1], x3[1])))), x4[1])))∧(x4[2] →^* java.lang.Object(Alternate.Tree(x5[1], x6[1])))∧(x5[2] →^* java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[1], x3[1]))))))

(2) -> (2), if ((2870_0_copy_Load(x5[2]) →^* 7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[2]', x1[2]')), NULL))))∧(java.lang.Object(Alternate.Tree(x5[2], x6[2])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[2]', x3[2]')), NULL)), x4[2]')))∧(x4[2] →^* java.lang.Object(Alternate.Tree(x5[2]', x6[2]')))∧(x5[2] →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[2]', x3[2]')), NULL))))

(2) -> (3), if ((2870_0_copy_Load(x5[2]) →^* 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[3], x1[3])), java.lang.Object(Alternate.Tree(x2[3], x3[3]))))))∧(java.lang.Object(Alternate.Tree(x5[2], x6[2])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[3], x5[3])), java.lang.Object(Alternate.Tree(x6[3], x7[3])))), x8[3])))∧(x4[2] →^* java.lang.Object(Alternate.Tree(x9[3], x10[3])))∧(x5[2] →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[3], x5[3])), java.lang.Object(Alternate.Tree(x6[3], x7[3]))))))

(2) -> (4), if ((2870_0_copy_Load(x5[2]) →^* 3543_0_copy_Return)∧(java.lang.Object(Alternate.Tree(x5[2], x6[2])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0[4])))∧(x4[2] →^* java.lang.Object(Alternate.Tree(x1[4], x2[4])))∧(x5[2] →^* java.lang.Object(Alternate.Tree(NULL, NULL))))

(3) -> (0), if ((2870_0_copy_Load(x9[3]) →^* 2875_0_copy_Return)∧(java.lang.Object(Alternate.Tree(x9[3], x10[3])) →^* java.lang.Object(Alternate.Tree(NULL, x0[0])))∧(x8[3] →^* java.lang.Object(Alternate.Tree(x1[0], x2[0])))∧(x9[3] →^* NULL))

(3) -> (1), if ((2870_0_copy_Load(x9[3]) →^* 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0[1], x1[1]))))))∧(java.lang.Object(Alternate.Tree(x9[3], x10[3])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[1], x3[1])))), x4[1])))∧(x8[3] →^* java.lang.Object(Alternate.Tree(x5[1], x6[1])))∧(x9[3] →^* java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[1], x3[1]))))))

(3) -> (2), if ((2870_0_copy_Load(x9[3]) →^* 7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[2], x1[2])), NULL))))∧(java.lang.Object(Alternate.Tree(x9[3], x10[3])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[2], x3[2])), NULL)), x4[2])))∧(x8[3] →^* java.lang.Object(Alternate.Tree(x5[2], x6[2])))∧(x9[3] →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[2], x3[2])), NULL))))

(3) -> (3), if ((2870_0_copy_Load(x9[3]) →^* 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[3]', x1[3]')), java.lang.Object(Alternate.Tree(x2[3]', x3[3]'))))))∧(java.lang.Object(Alternate.Tree(x9[3], x10[3])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[3]', x5[3]')), java.lang.Object(Alternate.Tree(x6[3]', x7[3]')))), x8[3]')))∧(x8[3] →^* java.lang.Object(Alternate.Tree(x9[3]', x10[3]')))∧(x9[3] →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[3]', x5[3]')), java.lang.Object(Alternate.Tree(x6[3]', x7[3]'))))))

(3) -> (4), if ((2870_0_copy_Load(x9[3]) →^* 3543_0_copy_Return)∧(java.lang.Object(Alternate.Tree(x9[3], x10[3])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0[4])))∧(x8[3] →^* java.lang.Object(Alternate.Tree(x1[4], x2[4])))∧(x9[3] →^* java.lang.Object(Alternate.Tree(NULL, NULL))))

(4) -> (0), if ((2870_0_copy_Load(x1[4]) →^* 2875_0_copy_Return)∧(java.lang.Object(Alternate.Tree(x1[4], x2[4])) →^* java.lang.Object(Alternate.Tree(NULL, x0[0])))∧(x0[4] →^* java.lang.Object(Alternate.Tree(x1[0], x2[0])))∧(x1[4] →^* NULL))

(4) -> (1), if ((2870_0_copy_Load(x1[4]) →^* 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0[1], x1[1]))))))∧(java.lang.Object(Alternate.Tree(x1[4], x2[4])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[1], x3[1])))), x4[1])))∧(x0[4] →^* java.lang.Object(Alternate.Tree(x5[1], x6[1])))∧(x1[4] →^* java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[1], x3[1]))))))

(4) -> (2), if ((2870_0_copy_Load(x1[4]) →^* 7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[2], x1[2])), NULL))))∧(java.lang.Object(Alternate.Tree(x1[4], x2[4])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[2], x3[2])), NULL)), x4[2])))∧(x0[4] →^* java.lang.Object(Alternate.Tree(x5[2], x6[2])))∧(x1[4] →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[2], x3[2])), NULL))))

(4) -> (3), if ((2870_0_copy_Load(x1[4]) →^* 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[3], x1[3])), java.lang.Object(Alternate.Tree(x2[3], x3[3]))))))∧(java.lang.Object(Alternate.Tree(x1[4], x2[4])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[3], x5[3])), java.lang.Object(Alternate.Tree(x6[3], x7[3])))), x8[3])))∧(x0[4] →^* java.lang.Object(Alternate.Tree(x9[3], x10[3])))∧(x1[4] →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[3], x5[3])), java.lang.Object(Alternate.Tree(x6[3], x7[3]))))))

(4) -> (4), if ((2870_0_copy_Load(x1[4]) →^* 3543_0_copy_Return)∧(java.lang.Object(Alternate.Tree(x1[4], x2[4])) →^* java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0[4]')))∧(x0[4] →^* java.lang.Object(Alternate.Tree(x1[4]', x2[4]')))∧(x1[4] →^* java.lang.Object(Alternate.Tree(NULL, NULL))))

The set Q consists of the following terms:
2870_0_copy_Load(x0)
3030_1_alternate_InvokeMethod(6204_0_alternate_Return(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))), NULL, java.lang.Object(Alternate.Tree(x0, x1)))
3030_1_alternate_InvokeMethod(7575_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))), NULL)
3030_1_alternate_InvokeMethod(8181_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))), NULL)
3030_1_alternate_InvokeMethod(10743_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, java.lang.Object(Alternate.Tree(x1, x2))))))), java.lang.Object(Alternate.Tree(NULL, x3)), java.lang.Object(Alternate.Tree(x4, x5)))
3030_1_alternate_InvokeMethod(10759_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, java.lang.Object(Alternate.Tree(x3, x4))))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x5, x6)), x7)), java.lang.Object(Alternate.Tree(x8, x9)))
6561_1_alternate_InvokeMethod(6204_0_alternate_Return(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))), java.lang.Object(Alternate.Tree(x4, x5)), NULL, java.lang.Object(Alternate.Tree(x0, x1)))
6561_1_alternate_InvokeMethod(7575_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5)))), NULL)
6561_1_alternate_InvokeMethod(8181_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9)))), NULL)
6561_1_alternate_InvokeMethod(10743_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, java.lang.Object(Alternate.Tree(x1, x2))))))), java.lang.Object(Alternate.Tree(x3, x4)), java.lang.Object(Alternate.Tree(NULL, x5)), java.lang.Object(Alternate.Tree(x6, x7)))
6561_1_alternate_InvokeMethod(10759_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, java.lang.Object(Alternate.Tree(x3, x4))))))), java.lang.Object(Alternate.Tree(x5, x6)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x7, x8)), x9)), java.lang.Object(Alternate.Tree(x10, x11)))
2799_0_copy_NONNULL(NULL)
2799_0_copy_NONNULL(java.lang.Object(Alternate.Tree(x0, x1)))
3131_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))), x4)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))))
3131_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), x4)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)))
3131_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))), x8)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))))
3131_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0)), java.lang.Object(Alternate.Tree(NULL, NULL)))
6648_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)))
6648_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9)))))
6648_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), java.lang.Object(Alternate.Tree(NULL, NULL)))
6648_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5)))))
6648_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), NULL)
3131_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, x0)), NULL)
3377_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))))
3377_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)))
3377_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))))
3377_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, NULL)))
3377_1_copy_InvokeMethod(2875_0_copy_Return, NULL)

(17) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

2870_1_ALTERNATE_INVOKEMETHOD(2875_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, x0[0])), java.lang.Object(Alternate.Tree(x1[0], x2[0])), NULL) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x1[0]), java.lang.Object(Alternate.Tree(x1[0], x2[0])), x0[0], x1[0])
2870_1_ALTERNATE_INVOKEMETHOD(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0[1], x1[1]))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[1], x3[1])))), x4[1])), java.lang.Object(Alternate.Tree(x5[1], x6[1])), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[1], x3[1]))))) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x5[1]), java.lang.Object(Alternate.Tree(x5[1], x6[1])), x4[1], x5[1])
2870_1_ALTERNATE_INVOKEMETHOD(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[2], x1[2])), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[2], x3[2])), NULL)), x4[2])), java.lang.Object(Alternate.Tree(x5[2], x6[2])), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[2], x3[2])), NULL))) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x5[2]), java.lang.Object(Alternate.Tree(x5[2], x6[2])), x4[2], x5[2])
2870_1_ALTERNATE_INVOKEMETHOD(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[3], x1[3])), java.lang.Object(Alternate.Tree(x2[3], x3[3]))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[3], x5[3])), java.lang.Object(Alternate.Tree(x6[3], x7[3])))), x8[3])), java.lang.Object(Alternate.Tree(x9[3], x10[3])), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[3], x5[3])), java.lang.Object(Alternate.Tree(x6[3], x7[3]))))) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x9[3]), java.lang.Object(Alternate.Tree(x9[3], x10[3])), x8[3], x9[3])
2870_1_ALTERNATE_INVOKEMETHOD(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0[4])), java.lang.Object(Alternate.Tree(x1[4], x2[4])), java.lang.Object(Alternate.Tree(NULL, NULL))) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x1[4]), java.lang.Object(Alternate.Tree(x1[4], x2[4])), x0[4], x1[4])

The TRS R consists of the following rules:

2870_0_copy_Load(x0) → 2799_0_copy_NONNULL(x0)
3030_1_alternate_InvokeMethod(6204_0_alternate_Return(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))), NULL, java.lang.Object(Alternate.Tree(x0, x1))) → 7575_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))))
3030_1_alternate_InvokeMethod(7575_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))), NULL) → 10743_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))))))
3030_1_alternate_InvokeMethod(8181_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))), NULL) → 10743_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))))))
3030_1_alternate_InvokeMethod(10743_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, java.lang.Object(Alternate.Tree(x1, x2))))))), java.lang.Object(Alternate.Tree(NULL, x3)), java.lang.Object(Alternate.Tree(x4, x5))) → 10743_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, java.lang.Object(Alternate.Tree(x1, x2)))))))))
3030_1_alternate_InvokeMethod(10759_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, java.lang.Object(Alternate.Tree(x3, x4))))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x5, x6)), x7)), java.lang.Object(Alternate.Tree(x8, x9))) → 10743_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, java.lang.Object(Alternate.Tree(x3, x4)))))))))
6561_1_alternate_InvokeMethod(6204_0_alternate_Return(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))), java.lang.Object(Alternate.Tree(x4, x5)), NULL, java.lang.Object(Alternate.Tree(x0, x1))) → 8181_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x2, x3)))))
6561_1_alternate_InvokeMethod(7575_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5)))), NULL) → 10759_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))))))
6561_1_alternate_InvokeMethod(8181_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9)))), NULL) → 10759_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))))))
6561_1_alternate_InvokeMethod(10743_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, java.lang.Object(Alternate.Tree(x1, x2))))))), java.lang.Object(Alternate.Tree(x3, x4)), java.lang.Object(Alternate.Tree(NULL, x5)), java.lang.Object(Alternate.Tree(x6, x7))) → 10759_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x3, x4)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, java.lang.Object(Alternate.Tree(x1, x2)))))))))
6561_1_alternate_InvokeMethod(10759_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, java.lang.Object(Alternate.Tree(x3, x4))))))), java.lang.Object(Alternate.Tree(x5, x6)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x7, x8)), x9)), java.lang.Object(Alternate.Tree(x10, x11))) → 10759_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x5, x6)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, java.lang.Object(Alternate.Tree(x3, x4)))))))))
2799_0_copy_NONNULL(NULL) → 2875_0_copy_Return
2799_0_copy_NONNULL(java.lang.Object(Alternate.Tree(x0, x1))) → 3131_1_copy_InvokeMethod(2799_0_copy_NONNULL(x0), java.lang.Object(Alternate.Tree(x0, x1)), x0)
3131_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))), x4)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3))))) → 6648_1_copy_InvokeMethod(2799_0_copy_NONNULL(x4), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))), NULL)), x4)
3131_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), x4)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL))) → 6648_1_copy_InvokeMethod(2799_0_copy_NONNULL(x4), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), NULL)), x4)
3131_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))), x8)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7))))) → 6648_1_copy_InvokeMethod(2799_0_copy_NONNULL(x8), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))), NULL)), x8)
3131_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0)), java.lang.Object(Alternate.Tree(NULL, NULL))) → 6648_1_copy_InvokeMethod(2799_0_copy_NONNULL(x0), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), NULL)), x0)
6648_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))))
6648_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9))))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))))))
6648_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), java.lang.Object(Alternate.Tree(NULL, NULL))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(NULL, NULL)))))
6648_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5))))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))))))
6648_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), NULL) → 7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))
3131_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, x0)), NULL) → 3377_1_copy_InvokeMethod(2799_0_copy_NONNULL(x0), x0)
3377_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3))))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))))))
3377_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))))
3377_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7))))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))))))
3377_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, NULL))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(NULL, NULL)))))
3377_1_copy_InvokeMethod(2875_0_copy_Return, NULL) → 3543_0_copy_Return

The set Q consists of the following terms:

2870_0_copy_Load(x0)
3030_1_alternate_InvokeMethod(6204_0_alternate_Return(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))), NULL, java.lang.Object(Alternate.Tree(x0, x1)))
3030_1_alternate_InvokeMethod(7575_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))), NULL)
3030_1_alternate_InvokeMethod(8181_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))), NULL)
3030_1_alternate_InvokeMethod(10743_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, java.lang.Object(Alternate.Tree(x1, x2))))))), java.lang.Object(Alternate.Tree(NULL, x3)), java.lang.Object(Alternate.Tree(x4, x5)))
3030_1_alternate_InvokeMethod(10759_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, java.lang.Object(Alternate.Tree(x3, x4))))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x5, x6)), x7)), java.lang.Object(Alternate.Tree(x8, x9)))
6561_1_alternate_InvokeMethod(6204_0_alternate_Return(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))), java.lang.Object(Alternate.Tree(x4, x5)), NULL, java.lang.Object(Alternate.Tree(x0, x1)))
6561_1_alternate_InvokeMethod(7575_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5)))), NULL)
6561_1_alternate_InvokeMethod(8181_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9)))), NULL)
6561_1_alternate_InvokeMethod(10743_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, java.lang.Object(Alternate.Tree(x1, x2))))))), java.lang.Object(Alternate.Tree(x3, x4)), java.lang.Object(Alternate.Tree(NULL, x5)), java.lang.Object(Alternate.Tree(x6, x7)))
6561_1_alternate_InvokeMethod(10759_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, java.lang.Object(Alternate.Tree(x3, x4))))))), java.lang.Object(Alternate.Tree(x5, x6)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x7, x8)), x9)), java.lang.Object(Alternate.Tree(x10, x11)))
2799_0_copy_NONNULL(NULL)
2799_0_copy_NONNULL(java.lang.Object(Alternate.Tree(x0, x1)))
3131_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))), x4)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))))
3131_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), x4)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)))
3131_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))), x8)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))))
3131_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0)), java.lang.Object(Alternate.Tree(NULL, NULL)))
6648_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)))
6648_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9)))))
6648_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), java.lang.Object(Alternate.Tree(NULL, NULL)))
6648_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5)))))
6648_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), NULL)
3131_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, x0)), NULL)
3377_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))))
3377_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)))
3377_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))))
3377_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, NULL)))
3377_1_copy_InvokeMethod(2875_0_copy_Return, NULL)

We have to consider all minimal (P,Q,R)-chains.

(19) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

2870_1_ALTERNATE_INVOKEMETHOD(2875_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, x0[0])), java.lang.Object(Alternate.Tree(x1[0], x2[0])), NULL) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x1[0]), java.lang.Object(Alternate.Tree(x1[0], x2[0])), x0[0], x1[0])
2870_1_ALTERNATE_INVOKEMETHOD(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0[1], x1[1]))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[1], x3[1])))), x4[1])), java.lang.Object(Alternate.Tree(x5[1], x6[1])), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[1], x3[1]))))) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x5[1]), java.lang.Object(Alternate.Tree(x5[1], x6[1])), x4[1], x5[1])
2870_1_ALTERNATE_INVOKEMETHOD(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[2], x1[2])), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[2], x3[2])), NULL)), x4[2])), java.lang.Object(Alternate.Tree(x5[2], x6[2])), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[2], x3[2])), NULL))) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x5[2]), java.lang.Object(Alternate.Tree(x5[2], x6[2])), x4[2], x5[2])
2870_1_ALTERNATE_INVOKEMETHOD(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[3], x1[3])), java.lang.Object(Alternate.Tree(x2[3], x3[3]))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[3], x5[3])), java.lang.Object(Alternate.Tree(x6[3], x7[3])))), x8[3])), java.lang.Object(Alternate.Tree(x9[3], x10[3])), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[3], x5[3])), java.lang.Object(Alternate.Tree(x6[3], x7[3]))))) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x9[3]), java.lang.Object(Alternate.Tree(x9[3], x10[3])), x8[3], x9[3])
2870_1_ALTERNATE_INVOKEMETHOD(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0[4])), java.lang.Object(Alternate.Tree(x1[4], x2[4])), java.lang.Object(Alternate.Tree(NULL, NULL))) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x1[4]), java.lang.Object(Alternate.Tree(x1[4], x2[4])), x0[4], x1[4])

The TRS R consists of the following rules:

2870_0_copy_Load(x0) → 2799_0_copy_NONNULL(x0)
2799_0_copy_NONNULL(NULL) → 2875_0_copy_Return
2799_0_copy_NONNULL(java.lang.Object(Alternate.Tree(x0, x1))) → 3131_1_copy_InvokeMethod(2799_0_copy_NONNULL(x0), java.lang.Object(Alternate.Tree(x0, x1)), x0)
3131_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))), x4)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3))))) → 6648_1_copy_InvokeMethod(2799_0_copy_NONNULL(x4), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))), NULL)), x4)
3131_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), x4)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL))) → 6648_1_copy_InvokeMethod(2799_0_copy_NONNULL(x4), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), NULL)), x4)
3131_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))), x8)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7))))) → 6648_1_copy_InvokeMethod(2799_0_copy_NONNULL(x8), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))), NULL)), x8)
3131_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0)), java.lang.Object(Alternate.Tree(NULL, NULL))) → 6648_1_copy_InvokeMethod(2799_0_copy_NONNULL(x0), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), NULL)), x0)
3131_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, x0)), NULL) → 3377_1_copy_InvokeMethod(2799_0_copy_NONNULL(x0), x0)
3377_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3))))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))))))
3377_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))))
3377_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7))))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))))))
3377_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, NULL))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(NULL, NULL)))))
3377_1_copy_InvokeMethod(2875_0_copy_Return, NULL) → 3543_0_copy_Return
6648_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))))
6648_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9))))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))))))
6648_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), java.lang.Object(Alternate.Tree(NULL, NULL))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(NULL, NULL)))))
6648_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5))))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))))))
6648_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), NULL) → 7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))

The set Q consists of the following terms:

2870_0_copy_Load(x0)
3030_1_alternate_InvokeMethod(6204_0_alternate_Return(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))), NULL, java.lang.Object(Alternate.Tree(x0, x1)))
3030_1_alternate_InvokeMethod(7575_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))), NULL)
3030_1_alternate_InvokeMethod(8181_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))), NULL)
3030_1_alternate_InvokeMethod(10743_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, java.lang.Object(Alternate.Tree(x1, x2))))))), java.lang.Object(Alternate.Tree(NULL, x3)), java.lang.Object(Alternate.Tree(x4, x5)))
3030_1_alternate_InvokeMethod(10759_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, java.lang.Object(Alternate.Tree(x3, x4))))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x5, x6)), x7)), java.lang.Object(Alternate.Tree(x8, x9)))
6561_1_alternate_InvokeMethod(6204_0_alternate_Return(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))), java.lang.Object(Alternate.Tree(x4, x5)), NULL, java.lang.Object(Alternate.Tree(x0, x1)))
6561_1_alternate_InvokeMethod(7575_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5)))), NULL)
6561_1_alternate_InvokeMethod(8181_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9)))), NULL)
6561_1_alternate_InvokeMethod(10743_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, java.lang.Object(Alternate.Tree(x1, x2))))))), java.lang.Object(Alternate.Tree(x3, x4)), java.lang.Object(Alternate.Tree(NULL, x5)), java.lang.Object(Alternate.Tree(x6, x7)))
6561_1_alternate_InvokeMethod(10759_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, java.lang.Object(Alternate.Tree(x3, x4))))))), java.lang.Object(Alternate.Tree(x5, x6)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x7, x8)), x9)), java.lang.Object(Alternate.Tree(x10, x11)))
2799_0_copy_NONNULL(NULL)
2799_0_copy_NONNULL(java.lang.Object(Alternate.Tree(x0, x1)))
3131_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))), x4)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))))
3131_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), x4)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)))
3131_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))), x8)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))))
3131_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0)), java.lang.Object(Alternate.Tree(NULL, NULL)))
6648_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)))
6648_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9)))))
6648_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), java.lang.Object(Alternate.Tree(NULL, NULL)))
6648_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5)))))
6648_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), NULL)
3131_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, x0)), NULL)
3377_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))))
3377_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)))
3377_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))))
3377_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, NULL)))
3377_1_copy_InvokeMethod(2875_0_copy_Return, NULL)

We have to consider all minimal (P,Q,R)-chains.

(21) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

3030_1_alternate_InvokeMethod(6204_0_alternate_Return(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))), NULL, java.lang.Object(Alternate.Tree(x0, x1)))
3030_1_alternate_InvokeMethod(7575_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))), NULL)
3030_1_alternate_InvokeMethod(8181_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))), NULL)
3030_1_alternate_InvokeMethod(10743_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, java.lang.Object(Alternate.Tree(x1, x2))))))), java.lang.Object(Alternate.Tree(NULL, x3)), java.lang.Object(Alternate.Tree(x4, x5)))
3030_1_alternate_InvokeMethod(10759_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, java.lang.Object(Alternate.Tree(x3, x4))))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x5, x6)), x7)), java.lang.Object(Alternate.Tree(x8, x9)))
6561_1_alternate_InvokeMethod(6204_0_alternate_Return(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))), java.lang.Object(Alternate.Tree(x4, x5)), NULL, java.lang.Object(Alternate.Tree(x0, x1)))
6561_1_alternate_InvokeMethod(7575_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5)))), NULL)
6561_1_alternate_InvokeMethod(8181_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9)))), NULL)
6561_1_alternate_InvokeMethod(10743_0_alternate_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, java.lang.Object(Alternate.Tree(x1, x2))))))), java.lang.Object(Alternate.Tree(x3, x4)), java.lang.Object(Alternate.Tree(NULL, x5)), java.lang.Object(Alternate.Tree(x6, x7)))
6561_1_alternate_InvokeMethod(10759_0_alternate_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, java.lang.Object(Alternate.Tree(x3, x4))))))), java.lang.Object(Alternate.Tree(x5, x6)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x7, x8)), x9)), java.lang.Object(Alternate.Tree(x10, x11)))

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

2870_1_ALTERNATE_INVOKEMETHOD(2875_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, x0[0])), java.lang.Object(Alternate.Tree(x1[0], x2[0])), NULL) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x1[0]), java.lang.Object(Alternate.Tree(x1[0], x2[0])), x0[0], x1[0])
2870_1_ALTERNATE_INVOKEMETHOD(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0[1], x1[1]))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[1], x3[1])))), x4[1])), java.lang.Object(Alternate.Tree(x5[1], x6[1])), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[1], x3[1]))))) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x5[1]), java.lang.Object(Alternate.Tree(x5[1], x6[1])), x4[1], x5[1])
2870_1_ALTERNATE_INVOKEMETHOD(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[2], x1[2])), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[2], x3[2])), NULL)), x4[2])), java.lang.Object(Alternate.Tree(x5[2], x6[2])), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[2], x3[2])), NULL))) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x5[2]), java.lang.Object(Alternate.Tree(x5[2], x6[2])), x4[2], x5[2])
2870_1_ALTERNATE_INVOKEMETHOD(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[3], x1[3])), java.lang.Object(Alternate.Tree(x2[3], x3[3]))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[3], x5[3])), java.lang.Object(Alternate.Tree(x6[3], x7[3])))), x8[3])), java.lang.Object(Alternate.Tree(x9[3], x10[3])), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[3], x5[3])), java.lang.Object(Alternate.Tree(x6[3], x7[3]))))) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x9[3]), java.lang.Object(Alternate.Tree(x9[3], x10[3])), x8[3], x9[3])
2870_1_ALTERNATE_INVOKEMETHOD(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0[4])), java.lang.Object(Alternate.Tree(x1[4], x2[4])), java.lang.Object(Alternate.Tree(NULL, NULL))) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x1[4]), java.lang.Object(Alternate.Tree(x1[4], x2[4])), x0[4], x1[4])

The TRS R consists of the following rules:

2870_0_copy_Load(x0) → 2799_0_copy_NONNULL(x0)
2799_0_copy_NONNULL(NULL) → 2875_0_copy_Return
2799_0_copy_NONNULL(java.lang.Object(Alternate.Tree(x0, x1))) → 3131_1_copy_InvokeMethod(2799_0_copy_NONNULL(x0), java.lang.Object(Alternate.Tree(x0, x1)), x0)
3131_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))), x4)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3))))) → 6648_1_copy_InvokeMethod(2799_0_copy_NONNULL(x4), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))), NULL)), x4)
3131_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), x4)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL))) → 6648_1_copy_InvokeMethod(2799_0_copy_NONNULL(x4), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), NULL)), x4)
3131_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))), x8)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7))))) → 6648_1_copy_InvokeMethod(2799_0_copy_NONNULL(x8), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))), NULL)), x8)
3131_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0)), java.lang.Object(Alternate.Tree(NULL, NULL))) → 6648_1_copy_InvokeMethod(2799_0_copy_NONNULL(x0), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), NULL)), x0)
3131_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, x0)), NULL) → 3377_1_copy_InvokeMethod(2799_0_copy_NONNULL(x0), x0)
3377_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3))))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))))))
3377_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))))
3377_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7))))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))))))
3377_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, NULL))) → 6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(NULL, NULL)))))
3377_1_copy_InvokeMethod(2875_0_copy_Return, NULL) → 3543_0_copy_Return
6648_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))))
6648_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9))))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3)))))))
6648_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), java.lang.Object(Alternate.Tree(NULL, NULL))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(NULL, NULL)))))
6648_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5))))) → 7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1)))))))
6648_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), NULL) → 7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)))

The set Q consists of the following terms:

2870_0_copy_Load(x0)
2799_0_copy_NONNULL(NULL)
2799_0_copy_NONNULL(java.lang.Object(Alternate.Tree(x0, x1)))
3131_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))), x4)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))))
3131_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), x4)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)))
3131_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))), x8)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))))
3131_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0)), java.lang.Object(Alternate.Tree(NULL, NULL)))
6648_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)))
6648_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), NULL)), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x6, x7)), java.lang.Object(Alternate.Tree(x8, x9)))))
6648_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), java.lang.Object(Alternate.Tree(NULL, NULL)))
6648_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x4, x5)))))
6648_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL)), NULL)
3131_1_copy_InvokeMethod(2875_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, x0)), NULL)
3377_1_copy_InvokeMethod(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0, x1))))), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2, x3)))))
3377_1_copy_InvokeMethod(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2, x3)), NULL)))
3377_1_copy_InvokeMethod(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0, x1)), java.lang.Object(Alternate.Tree(x2, x3))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4, x5)), java.lang.Object(Alternate.Tree(x6, x7)))))
3377_1_copy_InvokeMethod(3543_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, NULL)))
3377_1_copy_InvokeMethod(2875_0_copy_Return, NULL)

We have to consider all minimal (P,Q,R)-chains.

(23) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• 2870_1_ALTERNATE_INVOKEMETHOD(2875_0_copy_Return, java.lang.Object(Alternate.Tree(NULL, x0[0])), java.lang.Object(Alternate.Tree(x1[0], x2[0])), NULL) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x1[0]), java.lang.Object(Alternate.Tree(x1[0], x2[0])), x0[0], x1[0])
  The graph contains the following edges 3 >= 2, 2 > 3, 3 > 4

• 2870_1_ALTERNATE_INVOKEMETHOD(6379_0_copy_Return(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x0[1], x1[1]))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[1], x3[1])))), x4[1])), java.lang.Object(Alternate.Tree(x5[1], x6[1])), java.lang.Object(Alternate.Tree(NULL, java.lang.Object(Alternate.Tree(x2[1], x3[1]))))) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x5[1]), java.lang.Object(Alternate.Tree(x5[1], x6[1])), x4[1], x5[1])
  The graph contains the following edges 3 >= 2, 2 > 3, 3 > 4

• 2870_1_ALTERNATE_INVOKEMETHOD(7046_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[2], x1[2])), NULL))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[2], x3[2])), NULL)), x4[2])), java.lang.Object(Alternate.Tree(x5[2], x6[2])), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x2[2], x3[2])), NULL))) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x5[2]), java.lang.Object(Alternate.Tree(x5[2], x6[2])), x4[2], x5[2])
  The graph contains the following edges 3 >= 2, 2 > 3, 3 > 4

• 2870_1_ALTERNATE_INVOKEMETHOD(7594_0_copy_Return(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x0[3], x1[3])), java.lang.Object(Alternate.Tree(x2[3], x3[3]))))), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[3], x5[3])), java.lang.Object(Alternate.Tree(x6[3], x7[3])))), x8[3])), java.lang.Object(Alternate.Tree(x9[3], x10[3])), java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(x4[3], x5[3])), java.lang.Object(Alternate.Tree(x6[3], x7[3]))))) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x9[3]), java.lang.Object(Alternate.Tree(x9[3], x10[3])), x8[3], x9[3])
  The graph contains the following edges 3 >= 2, 2 > 3, 3 > 4

• 2870_1_ALTERNATE_INVOKEMETHOD(3543_0_copy_Return, java.lang.Object(Alternate.Tree(java.lang.Object(Alternate.Tree(NULL, NULL)), x0[4])), java.lang.Object(Alternate.Tree(x1[4], x2[4])), java.lang.Object(Alternate.Tree(NULL, NULL))) → 2870_1_ALTERNATE_INVOKEMETHOD(2870_0_copy_Load(x1[4]), java.lang.Object(Alternate.Tree(x1[4], x2[4])), x0[4], x1[4])
  The graph contains the following edges 3 >= 2, 2 > 3, 3 > 4

(24) YES

(25) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
16625_0_createNode_New → 18746_0_createNode_InvokeMethod
16625_0_createNode_New → 18521_0_createNode_InvokeMethod
16625_0_createNode_New → 18648_0_createNode_InvokeMethod
16625_0_createNode_New → 18547_0_createNode_InvokeMethod
15116_0_createTree_LE(0) → 15141_0_createTree_Return
16625_0_createNode_New → 2002_1_createNode_InvokeMethod
16625_1_createTree_InvokeMethod(2691_0_createNode_InvokeMethod, x0) → 16965_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 16965_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2691_0_createNode_InvokeMethod, x0) → 16424_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 16424_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2691_0_createNode_InvokeMethod, x0) → 16769_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 16769_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2691_0_createNode_InvokeMethod, x0) → 16489_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 16489_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 18960_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 18628_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 18807_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 18669_0_createTree_InvokeMethod(x0)
2002_1_createNode_InvokeMethod → 2177_0_createNode_Return
2002_1_createNode_InvokeMethod → 2691_0_createNode_InvokeMethod
2002_1_createNode_InvokeMethod → 2722_0_createNode_InvokeMethod
2002_1_createNode_InvokeMethod → 2552_0_createNode_Return

The integer pair graph contains the following rules and edges:
(0): 16625_1_CREATETREE_INVOKEMETHOD(2177_0_createNode_Return, x0[0]) → COND_16625_1_CREATETREE_INVOKEMETHOD(x0[0] > 0, 2177_0_createNode_Return, x0[0])
(1): COND_16625_1_CREATETREE_INVOKEMETHOD(TRUE, 2177_0_createNode_Return, x0[1]) → 15116_0_CREATETREE_LE(x0[1] + -1)
(2): 16625_1_CREATETREE_INVOKEMETHOD(2552_0_createNode_Return, x0[2]) → COND_16625_1_CREATETREE_INVOKEMETHOD1(x0[2] > 0, 2552_0_createNode_Return, x0[2])
(3): COND_16625_1_CREATETREE_INVOKEMETHOD1(TRUE, 2552_0_createNode_Return, x0[3]) → 15116_0_CREATETREE_LE(x0[3] + -1)
(4): 15116_0_CREATETREE_LE(x0[4]) → COND_15116_0_CREATETREE_LE(x0[4] > 0, x0[4])
(5): COND_15116_0_CREATETREE_LE(TRUE, x0[5]) → 15116_0_CREATETREE_LE(x0[5] + -1)
(6): 15116_0_CREATETREE_LE(x0[6]) → COND_15116_0_CREATETREE_LE1(x0[6] > 0, x0[6])
(7): COND_15116_0_CREATETREE_LE1(TRUE, x0[7]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[7])
(8): 15116_0_CREATETREE_LE(x0[8]) → COND_15116_0_CREATETREE_LE2(x0[8] > 0, x0[8])
(9): COND_15116_0_CREATETREE_LE2(TRUE, x0[9]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[9])
(10): 15116_0_CREATETREE_LE(x0[10]) → COND_15116_0_CREATETREE_LE3(x0[10] > 0, x0[10])
(11): COND_15116_0_CREATETREE_LE3(TRUE, x0[11]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[11])
(12): 15116_0_CREATETREE_LE(x0[12]) → COND_15116_0_CREATETREE_LE4(x0[12] > 0, x0[12])
(13): COND_15116_0_CREATETREE_LE4(TRUE, x0[13]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[13])
(14): 15116_0_CREATETREE_LE(x0[14]) → COND_15116_0_CREATETREE_LE5(x0[14] > 0, x0[14])
(15): COND_15116_0_CREATETREE_LE5(TRUE, x0[15]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[15])
(16): 15116_0_CREATETREE_LE(x0[16]) → COND_15116_0_CREATETREE_LE6(x0[16] > 0, x0[16])
(17): COND_15116_0_CREATETREE_LE6(TRUE, x0[17]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[17])
(18): 15116_0_CREATETREE_LE(x0[18]) → COND_15116_0_CREATETREE_LE7(x0[18] > 0, x0[18])
(19): COND_15116_0_CREATETREE_LE7(TRUE, x0[19]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[19])
(20): 15116_0_CREATETREE_LE(x0[20]) → COND_15116_0_CREATETREE_LE8(x0[20] > 0, x0[20])
(21): COND_15116_0_CREATETREE_LE8(TRUE, x0[21]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[21])

(0) -> (1), if ((x0[0] > 0 →^* TRUE)∧(x0[0] →^* x0[1]))

(1) -> (4), if ((x0[1] + -1 →^* x0[4]))

(1) -> (6), if ((x0[1] + -1 →^* x0[6]))

(1) -> (8), if ((x0[1] + -1 →^* x0[8]))

(1) -> (10), if ((x0[1] + -1 →^* x0[10]))

(1) -> (12), if ((x0[1] + -1 →^* x0[12]))

(1) -> (14), if ((x0[1] + -1 →^* x0[14]))

(1) -> (16), if ((x0[1] + -1 →^* x0[16]))

(1) -> (18), if ((x0[1] + -1 →^* x0[18]))

(1) -> (20), if ((x0[1] + -1 →^* x0[20]))

(2) -> (3), if ((x0[2] > 0 →^* TRUE)∧(x0[2] →^* x0[3]))

(3) -> (4), if ((x0[3] + -1 →^* x0[4]))

(3) -> (6), if ((x0[3] + -1 →^* x0[6]))

(3) -> (8), if ((x0[3] + -1 →^* x0[8]))

(3) -> (10), if ((x0[3] + -1 →^* x0[10]))

(3) -> (12), if ((x0[3] + -1 →^* x0[12]))

(3) -> (14), if ((x0[3] + -1 →^* x0[14]))

(3) -> (16), if ((x0[3] + -1 →^* x0[16]))

(3) -> (18), if ((x0[3] + -1 →^* x0[18]))

(3) -> (20), if ((x0[3] + -1 →^* x0[20]))

(4) -> (5), if ((x0[4] > 0 →^* TRUE)∧(x0[4] →^* x0[5]))

(5) -> (4), if ((x0[5] + -1 →^* x0[4]))

(5) -> (6), if ((x0[5] + -1 →^* x0[6]))

(5) -> (8), if ((x0[5] + -1 →^* x0[8]))

(5) -> (10), if ((x0[5] + -1 →^* x0[10]))

(5) -> (12), if ((x0[5] + -1 →^* x0[12]))

(5) -> (14), if ((x0[5] + -1 →^* x0[14]))

(5) -> (16), if ((x0[5] + -1 →^* x0[16]))

(5) -> (18), if ((x0[5] + -1 →^* x0[18]))

(5) -> (20), if ((x0[5] + -1 →^* x0[20]))

(6) -> (7), if ((x0[6] > 0 →^* TRUE)∧(x0[6] →^* x0[7]))

(7) -> (0), if ((16625_0_createNode_New →^* 2177_0_createNode_Return)∧(x0[7] →^* x0[0]))

(7) -> (2), if ((16625_0_createNode_New →^* 2552_0_createNode_Return)∧(x0[7] →^* x0[2]))

(8) -> (9), if ((x0[8] > 0 →^* TRUE)∧(x0[8] →^* x0[9]))

(9) -> (0), if ((16625_0_createNode_New →^* 2177_0_createNode_Return)∧(x0[9] →^* x0[0]))

(9) -> (2), if ((16625_0_createNode_New →^* 2552_0_createNode_Return)∧(x0[9] →^* x0[2]))

(10) -> (11), if ((x0[10] > 0 →^* TRUE)∧(x0[10] →^* x0[11]))

(11) -> (0), if ((16625_0_createNode_New →^* 2177_0_createNode_Return)∧(x0[11] →^* x0[0]))

(11) -> (2), if ((16625_0_createNode_New →^* 2552_0_createNode_Return)∧(x0[11] →^* x0[2]))

(12) -> (13), if ((x0[12] > 0 →^* TRUE)∧(x0[12] →^* x0[13]))

(13) -> (0), if ((16625_0_createNode_New →^* 2177_0_createNode_Return)∧(x0[13] →^* x0[0]))

(13) -> (2), if ((16625_0_createNode_New →^* 2552_0_createNode_Return)∧(x0[13] →^* x0[2]))

(14) -> (15), if ((x0[14] > 0 →^* TRUE)∧(x0[14] →^* x0[15]))

(15) -> (0), if ((16625_0_createNode_New →^* 2177_0_createNode_Return)∧(x0[15] →^* x0[0]))

(15) -> (2), if ((16625_0_createNode_New →^* 2552_0_createNode_Return)∧(x0[15] →^* x0[2]))

(16) -> (17), if ((x0[16] > 0 →^* TRUE)∧(x0[16] →^* x0[17]))

(17) -> (0), if ((16625_0_createNode_New →^* 2177_0_createNode_Return)∧(x0[17] →^* x0[0]))

(17) -> (2), if ((16625_0_createNode_New →^* 2552_0_createNode_Return)∧(x0[17] →^* x0[2]))

(18) -> (19), if ((x0[18] > 0 →^* TRUE)∧(x0[18] →^* x0[19]))

(19) -> (0), if ((16625_0_createNode_New →^* 2177_0_createNode_Return)∧(x0[19] →^* x0[0]))

(19) -> (2), if ((16625_0_createNode_New →^* 2552_0_createNode_Return)∧(x0[19] →^* x0[2]))

(20) -> (21), if ((x0[20] > 0 →^* TRUE)∧(x0[20] →^* x0[21]))

(21) -> (0), if ((16625_0_createNode_New →^* 2177_0_createNode_Return)∧(x0[21] →^* x0[0]))

(21) -> (2), if ((16625_0_createNode_New →^* 2552_0_createNode_Return)∧(x0[21] →^* x0[2]))

The set Q consists of the following terms:
16625_0_createNode_New
15116_0_createTree_LE(0)
16625_1_createTree_InvokeMethod(2691_0_createNode_InvokeMethod, x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0)
2002_1_createNode_InvokeMethod

(26) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair 16625_1_CREATETREE_INVOKEMETHOD(2177_0_createNode_Return, x0) → COND_16625_1_CREATETREE_INVOKEMETHOD(>(x0, 0), 2177_0_createNode_Return, x0) the following chains were created:

• We consider the chain 16625_1_CREATETREE_INVOKEMETHOD(2177_0_createNode_Return, x0[0]) → COND_16625_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 2177_0_createNode_Return, x0[0]), COND_16625_1_CREATETREE_INVOKEMETHOD(TRUE, 2177_0_createNode_Return, x0[1]) → 15116_0_CREATETREE_LE(+(x0[1], -1)) which results in the following constraint:
  

  (1)    (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 16625_1_CREATETREE_INVOKEMETHOD(2177_0_createNode_Return, x0[0])≥NonInfC∧16625_1_CREATETREE_INVOKEMETHOD(2177_0_createNode_Return, x0[0])≥COND_16625_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 2177_0_createNode_Return, x0[0])∧(U^Increasing(COND_16625_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 2177_0_createNode_Return, x0[0])), ≥))

  
  
  We simplified constraint (1) using rule (IV) which results in the following new constraint:
  

  (2)    (>(x0[0], 0)=TRUE ⇒ 16625_1_CREATETREE_INVOKEMETHOD(2177_0_createNode_Return, x0[0])≥NonInfC∧16625_1_CREATETREE_INVOKEMETHOD(2177_0_createNode_Return, x0[0])≥COND_16625_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 2177_0_createNode_Return, x0[0])∧(U^Increasing(COND_16625_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 2177_0_createNode_Return, x0[0])), ≥))

  
  
  We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (3)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_16625_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 2177_0_createNode_Return, x0[0])), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [(2)bni_51]x0[0] ≥ 0∧[(-1)bso_52] ≥ 0)

  
  
  We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (4)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_16625_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 2177_0_createNode_Return, x0[0])), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [(2)bni_51]x0[0] ≥ 0∧[(-1)bso_52] ≥ 0)

  
  
  We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (5)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_16625_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 2177_0_createNode_Return, x0[0])), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [(2)bni_51]x0[0] ≥ 0∧[(-1)bso_52] ≥ 0)

  
  
  We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (6)    (x0[0] ≥ 0 ⇒ (U^Increasing(COND_16625_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 2177_0_createNode_Return, x0[0])), ≥)∧[bni_51 + (-1)Bound*bni_51] + [(2)bni_51]x0[0] ≥ 0∧[(-1)bso_52] ≥ 0)

  
  
  

For Pair COND_16625_1_CREATETREE_INVOKEMETHOD(TRUE, 2177_0_createNode_Return, x0) → 15116_0_CREATETREE_LE(+(x0, -1)) the following chains were created:

• We consider the chain COND_16625_1_CREATETREE_INVOKEMETHOD(TRUE, 2177_0_createNode_Return, x0[1]) → 15116_0_CREATETREE_LE(+(x0[1], -1)) which results in the following constraint:
  

  (7)    (COND_16625_1_CREATETREE_INVOKEMETHOD(TRUE, 2177_0_createNode_Return, x0[1])≥NonInfC∧COND_16625_1_CREATETREE_INVOKEMETHOD(TRUE, 2177_0_createNode_Return, x0[1])≥15116_0_CREATETREE_LE(+(x0[1], -1))∧(U^Increasing(15116_0_CREATETREE_LE(+(x0[1], -1))), ≥))

  
  
  We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (8)    ((U^Increasing(15116_0_CREATETREE_LE(+(x0[1], -1))), ≥)∧[1 + (-1)bso_54] ≥ 0)

  
  
  We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (9)    ((U^Increasing(15116_0_CREATETREE_LE(+(x0[1], -1))), ≥)∧[1 + (-1)bso_54] ≥ 0)

  
  
  We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (10)    ((U^Increasing(15116_0_CREATETREE_LE(+(x0[1], -1))), ≥)∧[1 + (-1)bso_54] ≥ 0)

  
  
  We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (11)    ((U^Increasing(15116_0_CREATETREE_LE(+(x0[1], -1))), ≥)∧0 = 0∧[1 + (-1)bso_54] ≥ 0)

  
  
  

For Pair 16625_1_CREATETREE_INVOKEMETHOD(2552_0_createNode_Return, x0) → COND_16625_1_CREATETREE_INVOKEMETHOD1(>(x0, 0), 2552_0_createNode_Return, x0) the following chains were created:

• We consider the chain 16625_1_CREATETREE_INVOKEMETHOD(2552_0_createNode_Return, x0[2]) → COND_16625_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 2552_0_createNode_Return, x0[2]), COND_16625_1_CREATETREE_INVOKEMETHOD1(TRUE, 2552_0_createNode_Return, x0[3]) → 15116_0_CREATETREE_LE(+(x0[3], -1)) which results in the following constraint:
  

  (12)    (>(x0[2], 0)=TRUE∧x0[2]=x0[3] ⇒ 16625_1_CREATETREE_INVOKEMETHOD(2552_0_createNode_Return, x0[2])≥NonInfC∧16625_1_CREATETREE_INVOKEMETHOD(2552_0_createNode_Return, x0[2])≥COND_16625_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 2552_0_createNode_Return, x0[2])∧(U^Increasing(COND_16625_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 2552_0_createNode_Return, x0[2])), ≥))

  
  
  We simplified constraint (12) using rule (IV) which results in the following new constraint:
  

  (13)    (>(x0[2], 0)=TRUE ⇒ 16625_1_CREATETREE_INVOKEMETHOD(2552_0_createNode_Return, x0[2])≥NonInfC∧16625_1_CREATETREE_INVOKEMETHOD(2552_0_createNode_Return, x0[2])≥COND_16625_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 2552_0_createNode_Return, x0[2])∧(U^Increasing(COND_16625_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 2552_0_createNode_Return, x0[2])), ≥))

  
  
  We simplified constraint (13) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (14)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_16625_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 2552_0_createNode_Return, x0[2])), ≥)∧[(-1)bni_55 + (-1)Bound*bni_55] + [(2)bni_55]x0[2] ≥ 0∧[(-1)bso_56] ≥ 0)

  
  
  We simplified constraint (14) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (15)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_16625_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 2552_0_createNode_Return, x0[2])), ≥)∧[(-1)bni_55 + (-1)Bound*bni_55] + [(2)bni_55]x0[2] ≥ 0∧[(-1)bso_56] ≥ 0)

  
  
  We simplified constraint (15) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (16)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_16625_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 2552_0_createNode_Return, x0[2])), ≥)∧[(-1)bni_55 + (-1)Bound*bni_55] + [(2)bni_55]x0[2] ≥ 0∧[(-1)bso_56] ≥ 0)

  
  
  We simplified constraint (16) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (17)    (x0[2] ≥ 0 ⇒ (U^Increasing(COND_16625_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 2552_0_createNode_Return, x0[2])), ≥)∧[bni_55 + (-1)Bound*bni_55] + [(2)bni_55]x0[2] ≥ 0∧[(-1)bso_56] ≥ 0)

  
  
  

For Pair COND_16625_1_CREATETREE_INVOKEMETHOD1(TRUE, 2552_0_createNode_Return, x0) → 15116_0_CREATETREE_LE(+(x0, -1)) the following chains were created:

• We consider the chain COND_16625_1_CREATETREE_INVOKEMETHOD1(TRUE, 2552_0_createNode_Return, x0[3]) → 15116_0_CREATETREE_LE(+(x0[3], -1)) which results in the following constraint:
  

  (18)    (COND_16625_1_CREATETREE_INVOKEMETHOD1(TRUE, 2552_0_createNode_Return, x0[3])≥NonInfC∧COND_16625_1_CREATETREE_INVOKEMETHOD1(TRUE, 2552_0_createNode_Return, x0[3])≥15116_0_CREATETREE_LE(+(x0[3], -1))∧(U^Increasing(15116_0_CREATETREE_LE(+(x0[3], -1))), ≥))

  
  
  We simplified constraint (18) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (19)    ((U^Increasing(15116_0_CREATETREE_LE(+(x0[3], -1))), ≥)∧[1 + (-1)bso_58] ≥ 0)

  
  
  We simplified constraint (19) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (20)    ((U^Increasing(15116_0_CREATETREE_LE(+(x0[3], -1))), ≥)∧[1 + (-1)bso_58] ≥ 0)

  
  
  We simplified constraint (20) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (21)    ((U^Increasing(15116_0_CREATETREE_LE(+(x0[3], -1))), ≥)∧[1 + (-1)bso_58] ≥ 0)

  
  
  We simplified constraint (21) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (22)    ((U^Increasing(15116_0_CREATETREE_LE(+(x0[3], -1))), ≥)∧0 = 0∧[1 + (-1)bso_58] ≥ 0)

  
  
  

For Pair 15116_0_CREATETREE_LE(x0) → COND_15116_0_CREATETREE_LE(>(x0, 0), x0) the following chains were created:

• We consider the chain 15116_0_CREATETREE_LE(x0[4]) → COND_15116_0_CREATETREE_LE(>(x0[4], 0), x0[4]), COND_15116_0_CREATETREE_LE(TRUE, x0[5]) → 15116_0_CREATETREE_LE(+(x0[5], -1)) which results in the following constraint:
  

  (23)    (>(x0[4], 0)=TRUE∧x0[4]=x0[5] ⇒ 15116_0_CREATETREE_LE(x0[4])≥NonInfC∧15116_0_CREATETREE_LE(x0[4])≥COND_15116_0_CREATETREE_LE(>(x0[4], 0), x0[4])∧(U^Increasing(COND_15116_0_CREATETREE_LE(>(x0[4], 0), x0[4])), ≥))

  
  
  We simplified constraint (23) using rule (IV) which results in the following new constraint:
  

  (24)    (>(x0[4], 0)=TRUE ⇒ 15116_0_CREATETREE_LE(x0[4])≥NonInfC∧15116_0_CREATETREE_LE(x0[4])≥COND_15116_0_CREATETREE_LE(>(x0[4], 0), x0[4])∧(U^Increasing(COND_15116_0_CREATETREE_LE(>(x0[4], 0), x0[4])), ≥))

  
  
  We simplified constraint (24) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (25)    (x0[4] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE(>(x0[4], 0), x0[4])), ≥)∧[(-1)Bound*bni_59] + [(2)bni_59]x0[4] ≥ 0∧[1 + (-1)bso_60] ≥ 0)

  
  
  We simplified constraint (25) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (26)    (x0[4] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE(>(x0[4], 0), x0[4])), ≥)∧[(-1)Bound*bni_59] + [(2)bni_59]x0[4] ≥ 0∧[1 + (-1)bso_60] ≥ 0)

  
  
  We simplified constraint (26) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (27)    (x0[4] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE(>(x0[4], 0), x0[4])), ≥)∧[(-1)Bound*bni_59] + [(2)bni_59]x0[4] ≥ 0∧[1 + (-1)bso_60] ≥ 0)

  
  
  We simplified constraint (27) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (28)    (x0[4] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE(>(x0[4], 0), x0[4])), ≥)∧[(-1)Bound*bni_59 + (2)bni_59] + [(2)bni_59]x0[4] ≥ 0∧[1 + (-1)bso_60] ≥ 0)

  
  
  

For Pair COND_15116_0_CREATETREE_LE(TRUE, x0) → 15116_0_CREATETREE_LE(+(x0, -1)) the following chains were created:

• We consider the chain COND_15116_0_CREATETREE_LE(TRUE, x0[5]) → 15116_0_CREATETREE_LE(+(x0[5], -1)) which results in the following constraint:
  

  (29)    (COND_15116_0_CREATETREE_LE(TRUE, x0[5])≥NonInfC∧COND_15116_0_CREATETREE_LE(TRUE, x0[5])≥15116_0_CREATETREE_LE(+(x0[5], -1))∧(U^Increasing(15116_0_CREATETREE_LE(+(x0[5], -1))), ≥))

  
  
  We simplified constraint (29) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (30)    ((U^Increasing(15116_0_CREATETREE_LE(+(x0[5], -1))), ≥)∧[1 + (-1)bso_62] ≥ 0)

  
  
  We simplified constraint (30) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (31)    ((U^Increasing(15116_0_CREATETREE_LE(+(x0[5], -1))), ≥)∧[1 + (-1)bso_62] ≥ 0)

  
  
  We simplified constraint (31) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (32)    ((U^Increasing(15116_0_CREATETREE_LE(+(x0[5], -1))), ≥)∧[1 + (-1)bso_62] ≥ 0)

  
  
  We simplified constraint (32) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (33)    ((U^Increasing(15116_0_CREATETREE_LE(+(x0[5], -1))), ≥)∧0 = 0∧[1 + (-1)bso_62] ≥ 0)

  
  
  

For Pair 15116_0_CREATETREE_LE(x0) → COND_15116_0_CREATETREE_LE1(>(x0, 0), x0) the following chains were created:

• We consider the chain 15116_0_CREATETREE_LE(x0[6]) → COND_15116_0_CREATETREE_LE1(>(x0[6], 0), x0[6]), COND_15116_0_CREATETREE_LE1(TRUE, x0[7]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[7]) which results in the following constraint:
  

  (34)    (>(x0[6], 0)=TRUE∧x0[6]=x0[7] ⇒ 15116_0_CREATETREE_LE(x0[6])≥NonInfC∧15116_0_CREATETREE_LE(x0[6])≥COND_15116_0_CREATETREE_LE1(>(x0[6], 0), x0[6])∧(U^Increasing(COND_15116_0_CREATETREE_LE1(>(x0[6], 0), x0[6])), ≥))

  
  
  We simplified constraint (34) using rule (IV) which results in the following new constraint:
  

  (35)    (>(x0[6], 0)=TRUE ⇒ 15116_0_CREATETREE_LE(x0[6])≥NonInfC∧15116_0_CREATETREE_LE(x0[6])≥COND_15116_0_CREATETREE_LE1(>(x0[6], 0), x0[6])∧(U^Increasing(COND_15116_0_CREATETREE_LE1(>(x0[6], 0), x0[6])), ≥))

  
  
  We simplified constraint (35) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (36)    (x0[6] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE1(>(x0[6], 0), x0[6])), ≥)∧[(-1)Bound*bni_63] + [(2)bni_63]x0[6] ≥ 0∧[1 + (-1)bso_64] ≥ 0)

  
  
  We simplified constraint (36) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (37)    (x0[6] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE1(>(x0[6], 0), x0[6])), ≥)∧[(-1)Bound*bni_63] + [(2)bni_63]x0[6] ≥ 0∧[1 + (-1)bso_64] ≥ 0)

  
  
  We simplified constraint (37) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (38)    (x0[6] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE1(>(x0[6], 0), x0[6])), ≥)∧[(-1)Bound*bni_63] + [(2)bni_63]x0[6] ≥ 0∧[1 + (-1)bso_64] ≥ 0)

  
  
  We simplified constraint (38) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (39)    (x0[6] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE1(>(x0[6], 0), x0[6])), ≥)∧[(-1)Bound*bni_63 + (2)bni_63] + [(2)bni_63]x0[6] ≥ 0∧[1 + (-1)bso_64] ≥ 0)

  
  
  

For Pair COND_15116_0_CREATETREE_LE1(TRUE, x0) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0) the following chains were created:

• We consider the chain COND_15116_0_CREATETREE_LE1(TRUE, x0[7]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[7]) which results in the following constraint:
  

  (40)    (COND_15116_0_CREATETREE_LE1(TRUE, x0[7])≥NonInfC∧COND_15116_0_CREATETREE_LE1(TRUE, x0[7])≥16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[7])∧(U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[7])), ≥))

  
  
  We simplified constraint (40) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (41)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[7])), ≥)∧[(-1)bso_66] ≥ 0)

  
  
  We simplified constraint (41) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (42)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[7])), ≥)∧[(-1)bso_66] ≥ 0)

  
  
  We simplified constraint (42) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (43)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[7])), ≥)∧[(-1)bso_66] ≥ 0)

  
  
  We simplified constraint (43) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (44)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[7])), ≥)∧0 = 0∧[(-1)bso_66] ≥ 0)

  
  
  

For Pair 15116_0_CREATETREE_LE(x0) → COND_15116_0_CREATETREE_LE2(>(x0, 0), x0) the following chains were created:

• We consider the chain 15116_0_CREATETREE_LE(x0[8]) → COND_15116_0_CREATETREE_LE2(>(x0[8], 0), x0[8]), COND_15116_0_CREATETREE_LE2(TRUE, x0[9]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[9]) which results in the following constraint:
  

  (45)    (>(x0[8], 0)=TRUE∧x0[8]=x0[9] ⇒ 15116_0_CREATETREE_LE(x0[8])≥NonInfC∧15116_0_CREATETREE_LE(x0[8])≥COND_15116_0_CREATETREE_LE2(>(x0[8], 0), x0[8])∧(U^Increasing(COND_15116_0_CREATETREE_LE2(>(x0[8], 0), x0[8])), ≥))

  
  
  We simplified constraint (45) using rule (IV) which results in the following new constraint:
  

  (46)    (>(x0[8], 0)=TRUE ⇒ 15116_0_CREATETREE_LE(x0[8])≥NonInfC∧15116_0_CREATETREE_LE(x0[8])≥COND_15116_0_CREATETREE_LE2(>(x0[8], 0), x0[8])∧(U^Increasing(COND_15116_0_CREATETREE_LE2(>(x0[8], 0), x0[8])), ≥))

  
  
  We simplified constraint (46) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (47)    (x0[8] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE2(>(x0[8], 0), x0[8])), ≥)∧[(-1)Bound*bni_67] + [(2)bni_67]x0[8] ≥ 0∧[(-1)bso_68] ≥ 0)

  
  
  We simplified constraint (47) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (48)    (x0[8] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE2(>(x0[8], 0), x0[8])), ≥)∧[(-1)Bound*bni_67] + [(2)bni_67]x0[8] ≥ 0∧[(-1)bso_68] ≥ 0)

  
  
  We simplified constraint (48) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (49)    (x0[8] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE2(>(x0[8], 0), x0[8])), ≥)∧[(-1)Bound*bni_67] + [(2)bni_67]x0[8] ≥ 0∧[(-1)bso_68] ≥ 0)

  
  
  We simplified constraint (49) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (50)    (x0[8] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE2(>(x0[8], 0), x0[8])), ≥)∧[(-1)Bound*bni_67 + (2)bni_67] + [(2)bni_67]x0[8] ≥ 0∧[(-1)bso_68] ≥ 0)

  
  
  

For Pair COND_15116_0_CREATETREE_LE2(TRUE, x0) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0) the following chains were created:

• We consider the chain COND_15116_0_CREATETREE_LE2(TRUE, x0[9]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[9]) which results in the following constraint:
  

  (51)    (COND_15116_0_CREATETREE_LE2(TRUE, x0[9])≥NonInfC∧COND_15116_0_CREATETREE_LE2(TRUE, x0[9])≥16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[9])∧(U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[9])), ≥))

  
  
  We simplified constraint (51) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (52)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[9])), ≥)∧[1 + (-1)bso_70] ≥ 0)

  
  
  We simplified constraint (52) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (53)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[9])), ≥)∧[1 + (-1)bso_70] ≥ 0)

  
  
  We simplified constraint (53) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (54)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[9])), ≥)∧[1 + (-1)bso_70] ≥ 0)

  
  
  We simplified constraint (54) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (55)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[9])), ≥)∧0 = 0∧[1 + (-1)bso_70] ≥ 0)

  
  
  

For Pair 15116_0_CREATETREE_LE(x0) → COND_15116_0_CREATETREE_LE3(>(x0, 0), x0) the following chains were created:

• We consider the chain 15116_0_CREATETREE_LE(x0[10]) → COND_15116_0_CREATETREE_LE3(>(x0[10], 0), x0[10]), COND_15116_0_CREATETREE_LE3(TRUE, x0[11]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[11]) which results in the following constraint:
  

  (56)    (>(x0[10], 0)=TRUE∧x0[10]=x0[11] ⇒ 15116_0_CREATETREE_LE(x0[10])≥NonInfC∧15116_0_CREATETREE_LE(x0[10])≥COND_15116_0_CREATETREE_LE3(>(x0[10], 0), x0[10])∧(U^Increasing(COND_15116_0_CREATETREE_LE3(>(x0[10], 0), x0[10])), ≥))

  
  
  We simplified constraint (56) using rule (IV) which results in the following new constraint:
  

  (57)    (>(x0[10], 0)=TRUE ⇒ 15116_0_CREATETREE_LE(x0[10])≥NonInfC∧15116_0_CREATETREE_LE(x0[10])≥COND_15116_0_CREATETREE_LE3(>(x0[10], 0), x0[10])∧(U^Increasing(COND_15116_0_CREATETREE_LE3(>(x0[10], 0), x0[10])), ≥))

  
  
  We simplified constraint (57) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (58)    (x0[10] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE3(>(x0[10], 0), x0[10])), ≥)∧[(-1)Bound*bni_71] + [(2)bni_71]x0[10] ≥ 0∧[1 + (-1)bso_72] ≥ 0)

  
  
  We simplified constraint (58) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (59)    (x0[10] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE3(>(x0[10], 0), x0[10])), ≥)∧[(-1)Bound*bni_71] + [(2)bni_71]x0[10] ≥ 0∧[1 + (-1)bso_72] ≥ 0)

  
  
  We simplified constraint (59) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (60)    (x0[10] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE3(>(x0[10], 0), x0[10])), ≥)∧[(-1)Bound*bni_71] + [(2)bni_71]x0[10] ≥ 0∧[1 + (-1)bso_72] ≥ 0)

  
  
  We simplified constraint (60) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (61)    (x0[10] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE3(>(x0[10], 0), x0[10])), ≥)∧[(-1)Bound*bni_71 + (2)bni_71] + [(2)bni_71]x0[10] ≥ 0∧[1 + (-1)bso_72] ≥ 0)

  
  
  

For Pair COND_15116_0_CREATETREE_LE3(TRUE, x0) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0) the following chains were created:

• We consider the chain COND_15116_0_CREATETREE_LE3(TRUE, x0[11]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[11]) which results in the following constraint:
  

  (62)    (COND_15116_0_CREATETREE_LE3(TRUE, x0[11])≥NonInfC∧COND_15116_0_CREATETREE_LE3(TRUE, x0[11])≥16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[11])∧(U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[11])), ≥))

  
  
  We simplified constraint (62) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (63)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[11])), ≥)∧[(-1)bso_74] ≥ 0)

  
  
  We simplified constraint (63) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (64)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[11])), ≥)∧[(-1)bso_74] ≥ 0)

  
  
  We simplified constraint (64) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (65)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[11])), ≥)∧[(-1)bso_74] ≥ 0)

  
  
  We simplified constraint (65) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (66)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[11])), ≥)∧0 = 0∧[(-1)bso_74] ≥ 0)

  
  
  

For Pair 15116_0_CREATETREE_LE(x0) → COND_15116_0_CREATETREE_LE4(>(x0, 0), x0) the following chains were created:

• We consider the chain 15116_0_CREATETREE_LE(x0[12]) → COND_15116_0_CREATETREE_LE4(>(x0[12], 0), x0[12]), COND_15116_0_CREATETREE_LE4(TRUE, x0[13]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[13]) which results in the following constraint:
  

  (67)    (>(x0[12], 0)=TRUE∧x0[12]=x0[13] ⇒ 15116_0_CREATETREE_LE(x0[12])≥NonInfC∧15116_0_CREATETREE_LE(x0[12])≥COND_15116_0_CREATETREE_LE4(>(x0[12], 0), x0[12])∧(U^Increasing(COND_15116_0_CREATETREE_LE4(>(x0[12], 0), x0[12])), ≥))

  
  
  We simplified constraint (67) using rule (IV) which results in the following new constraint:
  

  (68)    (>(x0[12], 0)=TRUE ⇒ 15116_0_CREATETREE_LE(x0[12])≥NonInfC∧15116_0_CREATETREE_LE(x0[12])≥COND_15116_0_CREATETREE_LE4(>(x0[12], 0), x0[12])∧(U^Increasing(COND_15116_0_CREATETREE_LE4(>(x0[12], 0), x0[12])), ≥))

  
  
  We simplified constraint (68) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (69)    (x0[12] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE4(>(x0[12], 0), x0[12])), ≥)∧[(-1)Bound*bni_75] + [(2)bni_75]x0[12] ≥ 0∧[1 + (-1)bso_76] ≥ 0)

  
  
  We simplified constraint (69) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (70)    (x0[12] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE4(>(x0[12], 0), x0[12])), ≥)∧[(-1)Bound*bni_75] + [(2)bni_75]x0[12] ≥ 0∧[1 + (-1)bso_76] ≥ 0)

  
  
  We simplified constraint (70) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (71)    (x0[12] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE4(>(x0[12], 0), x0[12])), ≥)∧[(-1)Bound*bni_75] + [(2)bni_75]x0[12] ≥ 0∧[1 + (-1)bso_76] ≥ 0)

  
  
  We simplified constraint (71) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (72)    (x0[12] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE4(>(x0[12], 0), x0[12])), ≥)∧[(-1)Bound*bni_75 + (2)bni_75] + [(2)bni_75]x0[12] ≥ 0∧[1 + (-1)bso_76] ≥ 0)

  
  
  

For Pair COND_15116_0_CREATETREE_LE4(TRUE, x0) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0) the following chains were created:

• We consider the chain COND_15116_0_CREATETREE_LE4(TRUE, x0[13]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[13]) which results in the following constraint:
  

  (73)    (COND_15116_0_CREATETREE_LE4(TRUE, x0[13])≥NonInfC∧COND_15116_0_CREATETREE_LE4(TRUE, x0[13])≥16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[13])∧(U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[13])), ≥))

  
  
  We simplified constraint (73) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (74)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[13])), ≥)∧[(-1)bso_78] ≥ 0)

  
  
  We simplified constraint (74) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (75)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[13])), ≥)∧[(-1)bso_78] ≥ 0)

  
  
  We simplified constraint (75) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (76)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[13])), ≥)∧[(-1)bso_78] ≥ 0)

  
  
  We simplified constraint (76) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (77)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[13])), ≥)∧0 = 0∧[(-1)bso_78] ≥ 0)

  
  
  

For Pair 15116_0_CREATETREE_LE(x0) → COND_15116_0_CREATETREE_LE5(>(x0, 0), x0) the following chains were created:

• We consider the chain 15116_0_CREATETREE_LE(x0[14]) → COND_15116_0_CREATETREE_LE5(>(x0[14], 0), x0[14]), COND_15116_0_CREATETREE_LE5(TRUE, x0[15]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[15]) which results in the following constraint:
  

  (78)    (>(x0[14], 0)=TRUE∧x0[14]=x0[15] ⇒ 15116_0_CREATETREE_LE(x0[14])≥NonInfC∧15116_0_CREATETREE_LE(x0[14])≥COND_15116_0_CREATETREE_LE5(>(x0[14], 0), x0[14])∧(U^Increasing(COND_15116_0_CREATETREE_LE5(>(x0[14], 0), x0[14])), ≥))

  
  
  We simplified constraint (78) using rule (IV) which results in the following new constraint:
  

  (79)    (>(x0[14], 0)=TRUE ⇒ 15116_0_CREATETREE_LE(x0[14])≥NonInfC∧15116_0_CREATETREE_LE(x0[14])≥COND_15116_0_CREATETREE_LE5(>(x0[14], 0), x0[14])∧(U^Increasing(COND_15116_0_CREATETREE_LE5(>(x0[14], 0), x0[14])), ≥))

  
  
  We simplified constraint (79) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (80)    (x0[14] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE5(>(x0[14], 0), x0[14])), ≥)∧[(-1)Bound*bni_79] + [(2)bni_79]x0[14] ≥ 0∧[1 + (-1)bso_80] ≥ 0)

  
  
  We simplified constraint (80) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (81)    (x0[14] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE5(>(x0[14], 0), x0[14])), ≥)∧[(-1)Bound*bni_79] + [(2)bni_79]x0[14] ≥ 0∧[1 + (-1)bso_80] ≥ 0)

  
  
  We simplified constraint (81) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (82)    (x0[14] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE5(>(x0[14], 0), x0[14])), ≥)∧[(-1)Bound*bni_79] + [(2)bni_79]x0[14] ≥ 0∧[1 + (-1)bso_80] ≥ 0)

  
  
  We simplified constraint (82) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (83)    (x0[14] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE5(>(x0[14], 0), x0[14])), ≥)∧[(-1)Bound*bni_79 + (2)bni_79] + [(2)bni_79]x0[14] ≥ 0∧[1 + (-1)bso_80] ≥ 0)

  
  
  

For Pair COND_15116_0_CREATETREE_LE5(TRUE, x0) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0) the following chains were created:

• We consider the chain COND_15116_0_CREATETREE_LE5(TRUE, x0[15]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[15]) which results in the following constraint:
  

  (84)    (COND_15116_0_CREATETREE_LE5(TRUE, x0[15])≥NonInfC∧COND_15116_0_CREATETREE_LE5(TRUE, x0[15])≥16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[15])∧(U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[15])), ≥))

  
  
  We simplified constraint (84) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (85)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[15])), ≥)∧[(-1)bso_82] ≥ 0)

  
  
  We simplified constraint (85) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (86)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[15])), ≥)∧[(-1)bso_82] ≥ 0)

  
  
  We simplified constraint (86) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (87)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[15])), ≥)∧[(-1)bso_82] ≥ 0)

  
  
  We simplified constraint (87) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (88)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[15])), ≥)∧0 = 0∧[(-1)bso_82] ≥ 0)

  
  
  

For Pair 15116_0_CREATETREE_LE(x0) → COND_15116_0_CREATETREE_LE6(>(x0, 0), x0) the following chains were created:

• We consider the chain 15116_0_CREATETREE_LE(x0[16]) → COND_15116_0_CREATETREE_LE6(>(x0[16], 0), x0[16]), COND_15116_0_CREATETREE_LE6(TRUE, x0[17]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[17]) which results in the following constraint:
  

  (89)    (>(x0[16], 0)=TRUE∧x0[16]=x0[17] ⇒ 15116_0_CREATETREE_LE(x0[16])≥NonInfC∧15116_0_CREATETREE_LE(x0[16])≥COND_15116_0_CREATETREE_LE6(>(x0[16], 0), x0[16])∧(U^Increasing(COND_15116_0_CREATETREE_LE6(>(x0[16], 0), x0[16])), ≥))

  
  
  We simplified constraint (89) using rule (IV) which results in the following new constraint:
  

  (90)    (>(x0[16], 0)=TRUE ⇒ 15116_0_CREATETREE_LE(x0[16])≥NonInfC∧15116_0_CREATETREE_LE(x0[16])≥COND_15116_0_CREATETREE_LE6(>(x0[16], 0), x0[16])∧(U^Increasing(COND_15116_0_CREATETREE_LE6(>(x0[16], 0), x0[16])), ≥))

  
  
  We simplified constraint (90) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (91)    (x0[16] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE6(>(x0[16], 0), x0[16])), ≥)∧[(-1)Bound*bni_83] + [(2)bni_83]x0[16] ≥ 0∧[1 + (-1)bso_84] ≥ 0)

  
  
  We simplified constraint (91) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (92)    (x0[16] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE6(>(x0[16], 0), x0[16])), ≥)∧[(-1)Bound*bni_83] + [(2)bni_83]x0[16] ≥ 0∧[1 + (-1)bso_84] ≥ 0)

  
  
  We simplified constraint (92) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (93)    (x0[16] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE6(>(x0[16], 0), x0[16])), ≥)∧[(-1)Bound*bni_83] + [(2)bni_83]x0[16] ≥ 0∧[1 + (-1)bso_84] ≥ 0)

  
  
  We simplified constraint (93) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (94)    (x0[16] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE6(>(x0[16], 0), x0[16])), ≥)∧[(-1)Bound*bni_83 + (2)bni_83] + [(2)bni_83]x0[16] ≥ 0∧[1 + (-1)bso_84] ≥ 0)

  
  
  

For Pair COND_15116_0_CREATETREE_LE6(TRUE, x0) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0) the following chains were created:

• We consider the chain COND_15116_0_CREATETREE_LE6(TRUE, x0[17]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[17]) which results in the following constraint:
  

  (95)    (COND_15116_0_CREATETREE_LE6(TRUE, x0[17])≥NonInfC∧COND_15116_0_CREATETREE_LE6(TRUE, x0[17])≥16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[17])∧(U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[17])), ≥))

  
  
  We simplified constraint (95) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (96)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[17])), ≥)∧[(-1)bso_86] ≥ 0)

  
  
  We simplified constraint (96) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (97)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[17])), ≥)∧[(-1)bso_86] ≥ 0)

  
  
  We simplified constraint (97) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (98)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[17])), ≥)∧[(-1)bso_86] ≥ 0)

  
  
  We simplified constraint (98) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (99)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[17])), ≥)∧0 = 0∧[(-1)bso_86] ≥ 0)

  
  
  

For Pair 15116_0_CREATETREE_LE(x0) → COND_15116_0_CREATETREE_LE7(>(x0, 0), x0) the following chains were created:

• We consider the chain 15116_0_CREATETREE_LE(x0[18]) → COND_15116_0_CREATETREE_LE7(>(x0[18], 0), x0[18]), COND_15116_0_CREATETREE_LE7(TRUE, x0[19]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[19]) which results in the following constraint:
  

  (100)    (>(x0[18], 0)=TRUE∧x0[18]=x0[19] ⇒ 15116_0_CREATETREE_LE(x0[18])≥NonInfC∧15116_0_CREATETREE_LE(x0[18])≥COND_15116_0_CREATETREE_LE7(>(x0[18], 0), x0[18])∧(U^Increasing(COND_15116_0_CREATETREE_LE7(>(x0[18], 0), x0[18])), ≥))

  
  
  We simplified constraint (100) using rule (IV) which results in the following new constraint:
  

  (101)    (>(x0[18], 0)=TRUE ⇒ 15116_0_CREATETREE_LE(x0[18])≥NonInfC∧15116_0_CREATETREE_LE(x0[18])≥COND_15116_0_CREATETREE_LE7(>(x0[18], 0), x0[18])∧(U^Increasing(COND_15116_0_CREATETREE_LE7(>(x0[18], 0), x0[18])), ≥))

  
  
  We simplified constraint (101) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (102)    (x0[18] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE7(>(x0[18], 0), x0[18])), ≥)∧[(-1)Bound*bni_87] + [(2)bni_87]x0[18] ≥ 0∧[(-1)bso_88] ≥ 0)

  
  
  We simplified constraint (102) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (103)    (x0[18] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE7(>(x0[18], 0), x0[18])), ≥)∧[(-1)Bound*bni_87] + [(2)bni_87]x0[18] ≥ 0∧[(-1)bso_88] ≥ 0)

  
  
  We simplified constraint (103) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (104)    (x0[18] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE7(>(x0[18], 0), x0[18])), ≥)∧[(-1)Bound*bni_87] + [(2)bni_87]x0[18] ≥ 0∧[(-1)bso_88] ≥ 0)

  
  
  We simplified constraint (104) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (105)    (x0[18] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE7(>(x0[18], 0), x0[18])), ≥)∧[(-1)Bound*bni_87 + (2)bni_87] + [(2)bni_87]x0[18] ≥ 0∧[(-1)bso_88] ≥ 0)

  
  
  

For Pair COND_15116_0_CREATETREE_LE7(TRUE, x0) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0) the following chains were created:

• We consider the chain COND_15116_0_CREATETREE_LE7(TRUE, x0[19]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[19]) which results in the following constraint:
  

  (106)    (COND_15116_0_CREATETREE_LE7(TRUE, x0[19])≥NonInfC∧COND_15116_0_CREATETREE_LE7(TRUE, x0[19])≥16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[19])∧(U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[19])), ≥))

  
  
  We simplified constraint (106) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (107)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[19])), ≥)∧[1 + (-1)bso_90] ≥ 0)

  
  
  We simplified constraint (107) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (108)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[19])), ≥)∧[1 + (-1)bso_90] ≥ 0)

  
  
  We simplified constraint (108) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (109)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[19])), ≥)∧[1 + (-1)bso_90] ≥ 0)

  
  
  We simplified constraint (109) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (110)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[19])), ≥)∧0 = 0∧[1 + (-1)bso_90] ≥ 0)

  
  
  

For Pair 15116_0_CREATETREE_LE(x0) → COND_15116_0_CREATETREE_LE8(>(x0, 0), x0) the following chains were created:

• We consider the chain 15116_0_CREATETREE_LE(x0[20]) → COND_15116_0_CREATETREE_LE8(>(x0[20], 0), x0[20]), COND_15116_0_CREATETREE_LE8(TRUE, x0[21]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[21]) which results in the following constraint:
  

  (111)    (>(x0[20], 0)=TRUE∧x0[20]=x0[21] ⇒ 15116_0_CREATETREE_LE(x0[20])≥NonInfC∧15116_0_CREATETREE_LE(x0[20])≥COND_15116_0_CREATETREE_LE8(>(x0[20], 0), x0[20])∧(U^Increasing(COND_15116_0_CREATETREE_LE8(>(x0[20], 0), x0[20])), ≥))

  
  
  We simplified constraint (111) using rule (IV) which results in the following new constraint:
  

  (112)    (>(x0[20], 0)=TRUE ⇒ 15116_0_CREATETREE_LE(x0[20])≥NonInfC∧15116_0_CREATETREE_LE(x0[20])≥COND_15116_0_CREATETREE_LE8(>(x0[20], 0), x0[20])∧(U^Increasing(COND_15116_0_CREATETREE_LE8(>(x0[20], 0), x0[20])), ≥))

  
  
  We simplified constraint (112) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (113)    (x0[20] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE8(>(x0[20], 0), x0[20])), ≥)∧[(-1)Bound*bni_91] + [(2)bni_91]x0[20] ≥ 0∧[1 + (-1)bso_92] ≥ 0)

  
  
  We simplified constraint (113) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (114)    (x0[20] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE8(>(x0[20], 0), x0[20])), ≥)∧[(-1)Bound*bni_91] + [(2)bni_91]x0[20] ≥ 0∧[1 + (-1)bso_92] ≥ 0)

  
  
  We simplified constraint (114) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (115)    (x0[20] + [-1] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE8(>(x0[20], 0), x0[20])), ≥)∧[(-1)Bound*bni_91] + [(2)bni_91]x0[20] ≥ 0∧[1 + (-1)bso_92] ≥ 0)

  
  
  We simplified constraint (115) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (116)    (x0[20] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE8(>(x0[20], 0), x0[20])), ≥)∧[(-1)Bound*bni_91 + (2)bni_91] + [(2)bni_91]x0[20] ≥ 0∧[1 + (-1)bso_92] ≥ 0)

  
  
  

For Pair COND_15116_0_CREATETREE_LE8(TRUE, x0) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0) the following chains were created:

• We consider the chain COND_15116_0_CREATETREE_LE8(TRUE, x0[21]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[21]) which results in the following constraint:
  

  (117)    (COND_15116_0_CREATETREE_LE8(TRUE, x0[21])≥NonInfC∧COND_15116_0_CREATETREE_LE8(TRUE, x0[21])≥16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[21])∧(U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[21])), ≥))

  
  
  We simplified constraint (117) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (118)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[21])), ≥)∧[(-1)bso_94] ≥ 0)

  
  
  We simplified constraint (118) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (119)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[21])), ≥)∧[(-1)bso_94] ≥ 0)

  
  
  We simplified constraint (119) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (120)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[21])), ≥)∧[(-1)bso_94] ≥ 0)

  
  
  We simplified constraint (120) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (121)    ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[21])), ≥)∧0 = 0∧[(-1)bso_94] ≥ 0)

  
  
  

To summarize, we get the following constraints P_≥ for the following pairs.

• 16625_1_CREATETREE_INVOKEMETHOD(2177_0_createNode_Return, x0) → COND_16625_1_CREATETREE_INVOKEMETHOD(>(x0, 0), 2177_0_createNode_Return, x0)
  
  • (x0[0] ≥ 0 ⇒ (U^Increasing(COND_16625_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 2177_0_createNode_Return, x0[0])), ≥)∧[bni_51 + (-1)Bound*bni_51] + [(2)bni_51]x0[0] ≥ 0∧[(-1)bso_52] ≥ 0)
    
  
  
• COND_16625_1_CREATETREE_INVOKEMETHOD(TRUE, 2177_0_createNode_Return, x0) → 15116_0_CREATETREE_LE(+(x0, -1))
  
  • ((U^Increasing(15116_0_CREATETREE_LE(+(x0[1], -1))), ≥)∧0 = 0∧[1 + (-1)bso_54] ≥ 0)
    
  
  
• 16625_1_CREATETREE_INVOKEMETHOD(2552_0_createNode_Return, x0) → COND_16625_1_CREATETREE_INVOKEMETHOD1(>(x0, 0), 2552_0_createNode_Return, x0)
  
  • (x0[2] ≥ 0 ⇒ (U^Increasing(COND_16625_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 2552_0_createNode_Return, x0[2])), ≥)∧[bni_55 + (-1)Bound*bni_55] + [(2)bni_55]x0[2] ≥ 0∧[(-1)bso_56] ≥ 0)
    
  
  
• COND_16625_1_CREATETREE_INVOKEMETHOD1(TRUE, 2552_0_createNode_Return, x0) → 15116_0_CREATETREE_LE(+(x0, -1))
  
  • ((U^Increasing(15116_0_CREATETREE_LE(+(x0[3], -1))), ≥)∧0 = 0∧[1 + (-1)bso_58] ≥ 0)
    
  
  
• 15116_0_CREATETREE_LE(x0) → COND_15116_0_CREATETREE_LE(>(x0, 0), x0)
  
  • (x0[4] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE(>(x0[4], 0), x0[4])), ≥)∧[(-1)Bound*bni_59 + (2)bni_59] + [(2)bni_59]x0[4] ≥ 0∧[1 + (-1)bso_60] ≥ 0)
    
  
  
• COND_15116_0_CREATETREE_LE(TRUE, x0) → 15116_0_CREATETREE_LE(+(x0, -1))
  
  • ((U^Increasing(15116_0_CREATETREE_LE(+(x0[5], -1))), ≥)∧0 = 0∧[1 + (-1)bso_62] ≥ 0)
    
  
  
• 15116_0_CREATETREE_LE(x0) → COND_15116_0_CREATETREE_LE1(>(x0, 0), x0)
  
  • (x0[6] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE1(>(x0[6], 0), x0[6])), ≥)∧[(-1)Bound*bni_63 + (2)bni_63] + [(2)bni_63]x0[6] ≥ 0∧[1 + (-1)bso_64] ≥ 0)
    
  
  
• COND_15116_0_CREATETREE_LE1(TRUE, x0) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0)
  
  • ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[7])), ≥)∧0 = 0∧[(-1)bso_66] ≥ 0)
    
  
  
• 15116_0_CREATETREE_LE(x0) → COND_15116_0_CREATETREE_LE2(>(x0, 0), x0)
  
  • (x0[8] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE2(>(x0[8], 0), x0[8])), ≥)∧[(-1)Bound*bni_67 + (2)bni_67] + [(2)bni_67]x0[8] ≥ 0∧[(-1)bso_68] ≥ 0)
    
  
  
• COND_15116_0_CREATETREE_LE2(TRUE, x0) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0)
  
  • ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[9])), ≥)∧0 = 0∧[1 + (-1)bso_70] ≥ 0)
    
  
  
• 15116_0_CREATETREE_LE(x0) → COND_15116_0_CREATETREE_LE3(>(x0, 0), x0)
  
  • (x0[10] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE3(>(x0[10], 0), x0[10])), ≥)∧[(-1)Bound*bni_71 + (2)bni_71] + [(2)bni_71]x0[10] ≥ 0∧[1 + (-1)bso_72] ≥ 0)
    
  
  
• COND_15116_0_CREATETREE_LE3(TRUE, x0) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0)
  
  • ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[11])), ≥)∧0 = 0∧[(-1)bso_74] ≥ 0)
    
  
  
• 15116_0_CREATETREE_LE(x0) → COND_15116_0_CREATETREE_LE4(>(x0, 0), x0)
  
  • (x0[12] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE4(>(x0[12], 0), x0[12])), ≥)∧[(-1)Bound*bni_75 + (2)bni_75] + [(2)bni_75]x0[12] ≥ 0∧[1 + (-1)bso_76] ≥ 0)
    
  
  
• COND_15116_0_CREATETREE_LE4(TRUE, x0) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0)
  
  • ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[13])), ≥)∧0 = 0∧[(-1)bso_78] ≥ 0)
    
  
  
• 15116_0_CREATETREE_LE(x0) → COND_15116_0_CREATETREE_LE5(>(x0, 0), x0)
  
  • (x0[14] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE5(>(x0[14], 0), x0[14])), ≥)∧[(-1)Bound*bni_79 + (2)bni_79] + [(2)bni_79]x0[14] ≥ 0∧[1 + (-1)bso_80] ≥ 0)
    
  
  
• COND_15116_0_CREATETREE_LE5(TRUE, x0) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0)
  
  • ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[15])), ≥)∧0 = 0∧[(-1)bso_82] ≥ 0)
    
  
  
• 15116_0_CREATETREE_LE(x0) → COND_15116_0_CREATETREE_LE6(>(x0, 0), x0)
  
  • (x0[16] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE6(>(x0[16], 0), x0[16])), ≥)∧[(-1)Bound*bni_83 + (2)bni_83] + [(2)bni_83]x0[16] ≥ 0∧[1 + (-1)bso_84] ≥ 0)
    
  
  
• COND_15116_0_CREATETREE_LE6(TRUE, x0) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0)
  
  • ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[17])), ≥)∧0 = 0∧[(-1)bso_86] ≥ 0)
    
  
  
• 15116_0_CREATETREE_LE(x0) → COND_15116_0_CREATETREE_LE7(>(x0, 0), x0)
  
  • (x0[18] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE7(>(x0[18], 0), x0[18])), ≥)∧[(-1)Bound*bni_87 + (2)bni_87] + [(2)bni_87]x0[18] ≥ 0∧[(-1)bso_88] ≥ 0)
    
  
  
• COND_15116_0_CREATETREE_LE7(TRUE, x0) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0)
  
  • ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[19])), ≥)∧0 = 0∧[1 + (-1)bso_90] ≥ 0)
    
  
  
• 15116_0_CREATETREE_LE(x0) → COND_15116_0_CREATETREE_LE8(>(x0, 0), x0)
  
  • (x0[20] ≥ 0 ⇒ (U^Increasing(COND_15116_0_CREATETREE_LE8(>(x0[20], 0), x0[20])), ≥)∧[(-1)Bound*bni_91 + (2)bni_91] + [(2)bni_91]x0[20] ≥ 0∧[1 + (-1)bso_92] ≥ 0)
    
  
  
• COND_15116_0_CREATETREE_LE8(TRUE, x0) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0)
  
  • ((U^Increasing(16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[21])), ≥)∧0 = 0∧[(-1)bso_94] ≥ 0)
    
  
  

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(16625_0_createNode_New) = [-1]   
POL(18746_0_createNode_InvokeMethod) = [-1]   
POL(18521_0_createNode_InvokeMethod) = [-1]   
POL(18648_0_createNode_InvokeMethod) = [-1]   
POL(18547_0_createNode_InvokeMethod) = [-1]   
POL(15116_0_createTree_LE(x₁)) = [-1]   
POL(0) = 0   
POL(15141_0_createTree_Return) = [-1]   
POL(2002_1_createNode_InvokeMethod) = [-1]   
POL(16625_1_createTree_InvokeMethod(x₁, x₂)) = [-1]   
POL(2691_0_createNode_InvokeMethod) = [-1]   
POL(16965_0_createTree_InvokeMethod(x₁)) = [-1]   
POL(2722_0_createNode_InvokeMethod) = [-1]   
POL(16424_0_createTree_InvokeMethod(x₁)) = [-1]   
POL(16769_0_createTree_InvokeMethod(x₁)) = [-1]   
POL(16489_0_createTree_InvokeMethod(x₁)) = [-1]   
POL(18960_0_createTree_InvokeMethod(x₁)) = [-1]   
POL(18628_0_createTree_InvokeMethod(x₁)) = [-1]   
POL(18807_0_createTree_InvokeMethod(x₁)) = [-1]   
POL(18669_0_createTree_InvokeMethod(x₁)) = [-1]   
POL(2177_0_createNode_Return) = [-1]   
POL(2552_0_createNode_Return) = [-1]   
POL(16625_1_CREATETREE_INVOKEMETHOD(x₁, x₂)) = [-1] + [2]x₂   
POL(COND_16625_1_CREATETREE_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [2]x₃   
POL(>(x₁, x₂)) = [-1]   
POL(15116_0_CREATETREE_LE(x₁)) = [2]x₁   
POL(+(x₁, x₂)) = x₁ + x₂   
POL(-1) = [-1]   
POL(COND_16625_1_CREATETREE_INVOKEMETHOD1(x₁, x₂, x₃)) = [-1] + [2]x₃   
POL(COND_15116_0_CREATETREE_LE(x₁, x₂)) = [-1] + [2]x₂   
POL(COND_15116_0_CREATETREE_LE1(x₁, x₂)) = [-1] + [2]x₂   
POL(COND_15116_0_CREATETREE_LE2(x₁, x₂)) = [2]x₂   
POL(COND_15116_0_CREATETREE_LE3(x₁, x₂)) = [-1] + [2]x₂   
POL(COND_15116_0_CREATETREE_LE4(x₁, x₂)) = [-1] + [2]x₂   
POL(COND_15116_0_CREATETREE_LE5(x₁, x₂)) = [-1] + [2]x₂   
POL(COND_15116_0_CREATETREE_LE6(x₁, x₂)) = [-1] + [2]x₂   
POL(COND_15116_0_CREATETREE_LE7(x₁, x₂)) = [2]x₂   
POL(COND_15116_0_CREATETREE_LE8(x₁, x₂)) = [-1] + [2]x₂   

The following pairs are in P_>:

COND_16625_1_CREATETREE_INVOKEMETHOD(TRUE, 2177_0_createNode_Return, x0[1]) → 15116_0_CREATETREE_LE(+(x0[1], -1))
COND_16625_1_CREATETREE_INVOKEMETHOD1(TRUE, 2552_0_createNode_Return, x0[3]) → 15116_0_CREATETREE_LE(+(x0[3], -1))
15116_0_CREATETREE_LE(x0[4]) → COND_15116_0_CREATETREE_LE(>(x0[4], 0), x0[4])
COND_15116_0_CREATETREE_LE(TRUE, x0[5]) → 15116_0_CREATETREE_LE(+(x0[5], -1))
15116_0_CREATETREE_LE(x0[6]) → COND_15116_0_CREATETREE_LE1(>(x0[6], 0), x0[6])
COND_15116_0_CREATETREE_LE2(TRUE, x0[9]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[9])
15116_0_CREATETREE_LE(x0[10]) → COND_15116_0_CREATETREE_LE3(>(x0[10], 0), x0[10])
15116_0_CREATETREE_LE(x0[12]) → COND_15116_0_CREATETREE_LE4(>(x0[12], 0), x0[12])
15116_0_CREATETREE_LE(x0[14]) → COND_15116_0_CREATETREE_LE5(>(x0[14], 0), x0[14])
15116_0_CREATETREE_LE(x0[16]) → COND_15116_0_CREATETREE_LE6(>(x0[16], 0), x0[16])
COND_15116_0_CREATETREE_LE7(TRUE, x0[19]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[19])
15116_0_CREATETREE_LE(x0[20]) → COND_15116_0_CREATETREE_LE8(>(x0[20], 0), x0[20])

The following pairs are in P_bound:

16625_1_CREATETREE_INVOKEMETHOD(2177_0_createNode_Return, x0[0]) → COND_16625_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 2177_0_createNode_Return, x0[0])
16625_1_CREATETREE_INVOKEMETHOD(2552_0_createNode_Return, x0[2]) → COND_16625_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 2552_0_createNode_Return, x0[2])
15116_0_CREATETREE_LE(x0[4]) → COND_15116_0_CREATETREE_LE(>(x0[4], 0), x0[4])
15116_0_CREATETREE_LE(x0[6]) → COND_15116_0_CREATETREE_LE1(>(x0[6], 0), x0[6])
15116_0_CREATETREE_LE(x0[8]) → COND_15116_0_CREATETREE_LE2(>(x0[8], 0), x0[8])
15116_0_CREATETREE_LE(x0[10]) → COND_15116_0_CREATETREE_LE3(>(x0[10], 0), x0[10])
15116_0_CREATETREE_LE(x0[12]) → COND_15116_0_CREATETREE_LE4(>(x0[12], 0), x0[12])
15116_0_CREATETREE_LE(x0[14]) → COND_15116_0_CREATETREE_LE5(>(x0[14], 0), x0[14])
15116_0_CREATETREE_LE(x0[16]) → COND_15116_0_CREATETREE_LE6(>(x0[16], 0), x0[16])
15116_0_CREATETREE_LE(x0[18]) → COND_15116_0_CREATETREE_LE7(>(x0[18], 0), x0[18])
15116_0_CREATETREE_LE(x0[20]) → COND_15116_0_CREATETREE_LE8(>(x0[20], 0), x0[20])

The following pairs are in P_≥:

16625_1_CREATETREE_INVOKEMETHOD(2177_0_createNode_Return, x0[0]) → COND_16625_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 2177_0_createNode_Return, x0[0])
16625_1_CREATETREE_INVOKEMETHOD(2552_0_createNode_Return, x0[2]) → COND_16625_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 2552_0_createNode_Return, x0[2])
COND_15116_0_CREATETREE_LE1(TRUE, x0[7]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[7])
15116_0_CREATETREE_LE(x0[8]) → COND_15116_0_CREATETREE_LE2(>(x0[8], 0), x0[8])
COND_15116_0_CREATETREE_LE3(TRUE, x0[11]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[11])
COND_15116_0_CREATETREE_LE4(TRUE, x0[13]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[13])
COND_15116_0_CREATETREE_LE5(TRUE, x0[15]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[15])
COND_15116_0_CREATETREE_LE6(TRUE, x0[17]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[17])
15116_0_CREATETREE_LE(x0[18]) → COND_15116_0_CREATETREE_LE7(>(x0[18], 0), x0[18])
COND_15116_0_CREATETREE_LE8(TRUE, x0[21]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[21])

There are no usable rules.

(27) Complex Obligation (AND)

(28) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
16625_0_createNode_New → 18746_0_createNode_InvokeMethod
16625_0_createNode_New → 18521_0_createNode_InvokeMethod
16625_0_createNode_New → 18648_0_createNode_InvokeMethod
16625_0_createNode_New → 18547_0_createNode_InvokeMethod
15116_0_createTree_LE(0) → 15141_0_createTree_Return
16625_0_createNode_New → 2002_1_createNode_InvokeMethod
16625_1_createTree_InvokeMethod(2691_0_createNode_InvokeMethod, x0) → 16965_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 16965_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2691_0_createNode_InvokeMethod, x0) → 16424_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 16424_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2691_0_createNode_InvokeMethod, x0) → 16769_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 16769_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2691_0_createNode_InvokeMethod, x0) → 16489_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 16489_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 18960_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 18628_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 18807_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 18669_0_createTree_InvokeMethod(x0)
2002_1_createNode_InvokeMethod → 2177_0_createNode_Return
2002_1_createNode_InvokeMethod → 2691_0_createNode_InvokeMethod
2002_1_createNode_InvokeMethod → 2722_0_createNode_InvokeMethod
2002_1_createNode_InvokeMethod → 2552_0_createNode_Return

The integer pair graph contains the following rules and edges:
(0): 16625_1_CREATETREE_INVOKEMETHOD(2177_0_createNode_Return, x0[0]) → COND_16625_1_CREATETREE_INVOKEMETHOD(x0[0] > 0, 2177_0_createNode_Return, x0[0])
(2): 16625_1_CREATETREE_INVOKEMETHOD(2552_0_createNode_Return, x0[2]) → COND_16625_1_CREATETREE_INVOKEMETHOD1(x0[2] > 0, 2552_0_createNode_Return, x0[2])
(7): COND_15116_0_CREATETREE_LE1(TRUE, x0[7]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[7])
(8): 15116_0_CREATETREE_LE(x0[8]) → COND_15116_0_CREATETREE_LE2(x0[8] > 0, x0[8])
(11): COND_15116_0_CREATETREE_LE3(TRUE, x0[11]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[11])
(13): COND_15116_0_CREATETREE_LE4(TRUE, x0[13]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[13])
(15): COND_15116_0_CREATETREE_LE5(TRUE, x0[15]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[15])
(17): COND_15116_0_CREATETREE_LE6(TRUE, x0[17]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[17])
(18): 15116_0_CREATETREE_LE(x0[18]) → COND_15116_0_CREATETREE_LE7(x0[18] > 0, x0[18])
(21): COND_15116_0_CREATETREE_LE8(TRUE, x0[21]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[21])

(7) -> (0), if ((16625_0_createNode_New →^* 2177_0_createNode_Return)∧(x0[7] →^* x0[0]))

(11) -> (0), if ((16625_0_createNode_New →^* 2177_0_createNode_Return)∧(x0[11] →^* x0[0]))

(13) -> (0), if ((16625_0_createNode_New →^* 2177_0_createNode_Return)∧(x0[13] →^* x0[0]))

(15) -> (0), if ((16625_0_createNode_New →^* 2177_0_createNode_Return)∧(x0[15] →^* x0[0]))

(17) -> (0), if ((16625_0_createNode_New →^* 2177_0_createNode_Return)∧(x0[17] →^* x0[0]))

(21) -> (0), if ((16625_0_createNode_New →^* 2177_0_createNode_Return)∧(x0[21] →^* x0[0]))

(7) -> (2), if ((16625_0_createNode_New →^* 2552_0_createNode_Return)∧(x0[7] →^* x0[2]))

(11) -> (2), if ((16625_0_createNode_New →^* 2552_0_createNode_Return)∧(x0[11] →^* x0[2]))

(13) -> (2), if ((16625_0_createNode_New →^* 2552_0_createNode_Return)∧(x0[13] →^* x0[2]))

(15) -> (2), if ((16625_0_createNode_New →^* 2552_0_createNode_Return)∧(x0[15] →^* x0[2]))

(17) -> (2), if ((16625_0_createNode_New →^* 2552_0_createNode_Return)∧(x0[17] →^* x0[2]))

(21) -> (2), if ((16625_0_createNode_New →^* 2552_0_createNode_Return)∧(x0[21] →^* x0[2]))

The set Q consists of the following terms:
16625_0_createNode_New
15116_0_createTree_LE(0)
16625_1_createTree_InvokeMethod(2691_0_createNode_InvokeMethod, x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0)
2002_1_createNode_InvokeMethod

(29) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 10 less nodes.

(30) TRUE

(31) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
16625_0_createNode_New → 18746_0_createNode_InvokeMethod
16625_0_createNode_New → 18521_0_createNode_InvokeMethod
16625_0_createNode_New → 18648_0_createNode_InvokeMethod
16625_0_createNode_New → 18547_0_createNode_InvokeMethod
15116_0_createTree_LE(0) → 15141_0_createTree_Return
16625_0_createNode_New → 2002_1_createNode_InvokeMethod
16625_1_createTree_InvokeMethod(2691_0_createNode_InvokeMethod, x0) → 16965_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 16965_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2691_0_createNode_InvokeMethod, x0) → 16424_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 16424_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2691_0_createNode_InvokeMethod, x0) → 16769_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 16769_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2691_0_createNode_InvokeMethod, x0) → 16489_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 16489_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 18960_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 18628_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 18807_0_createTree_InvokeMethod(x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0) → 18669_0_createTree_InvokeMethod(x0)
2002_1_createNode_InvokeMethod → 2177_0_createNode_Return
2002_1_createNode_InvokeMethod → 2691_0_createNode_InvokeMethod
2002_1_createNode_InvokeMethod → 2722_0_createNode_InvokeMethod
2002_1_createNode_InvokeMethod → 2552_0_createNode_Return

The integer pair graph contains the following rules and edges:
(1): COND_16625_1_CREATETREE_INVOKEMETHOD(TRUE, 2177_0_createNode_Return, x0[1]) → 15116_0_CREATETREE_LE(x0[1] + -1)
(3): COND_16625_1_CREATETREE_INVOKEMETHOD1(TRUE, 2552_0_createNode_Return, x0[3]) → 15116_0_CREATETREE_LE(x0[3] + -1)
(5): COND_15116_0_CREATETREE_LE(TRUE, x0[5]) → 15116_0_CREATETREE_LE(x0[5] + -1)
(7): COND_15116_0_CREATETREE_LE1(TRUE, x0[7]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[7])
(9): COND_15116_0_CREATETREE_LE2(TRUE, x0[9]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[9])
(11): COND_15116_0_CREATETREE_LE3(TRUE, x0[11]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[11])
(13): COND_15116_0_CREATETREE_LE4(TRUE, x0[13]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[13])
(15): COND_15116_0_CREATETREE_LE5(TRUE, x0[15]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[15])
(17): COND_15116_0_CREATETREE_LE6(TRUE, x0[17]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[17])
(19): COND_15116_0_CREATETREE_LE7(TRUE, x0[19]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[19])
(21): COND_15116_0_CREATETREE_LE8(TRUE, x0[21]) → 16625_1_CREATETREE_INVOKEMETHOD(16625_0_createNode_New, x0[21])


The set Q consists of the following terms:
16625_0_createNode_New
15116_0_createTree_LE(0)
16625_1_createTree_InvokeMethod(2691_0_createNode_InvokeMethod, x0)
16625_1_createTree_InvokeMethod(2722_0_createNode_InvokeMethod, x0)
2002_1_createNode_InvokeMethod

(32) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 11 less nodes.

(33) TRUE